Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Alloy model of PSP data model
sig Defect {
phase : one Phase,
performance : one Performance,
type : one DefectType,
}
sig DefectType {}
fact DefectsBelongToAPhaseOfTheSameProcessAsItsPerformance {
all d : Defect | d.phase.process = d.performance.process
}
fact DefectsBelongToAPerformedPhase {
all d : Defect | d.phase in d.performance.performed_phases
}
sig OnTaskTime {
phase : one Phase,
performance : one Performance
}
fact OnTaskTimeBelongsToAPhaseOfTheSameProcessAsItsPerformance {
all ott : OnTaskTime | ott.phase.process = ott.performance.process
}
fact OnTaskTimeBelongsToAPerformedPhase {
all ott : OnTaskTime | ott.phase in ott.performance.performed_phases
}
sig Performance {
process : one Process,
performed_phases : some Phase,
time_logs : set OnTaskTime,
defect_logs : set Defect
}
fact PerformedPhasesAreASubsetOfProcessPhases {
all p : Performance | p.performed_phases in p.process.phases
}
fact PerformanceTimeLogsPointBackToIt {
all p : Performance | p.time_logs.performance = p
}
fact PerformanceDefectLogsPointBackToIt {
all p : Performance | p.defect_logs.performance = p
}
sig PhaseName {}
fact AllPhaseNamesBelongToSomePhase {
all pn : PhaseName | some p : Phase | p.name = pn
}
sig Phase {
name : one PhaseName,
process : one Process,
time_logs : set OnTaskTime,
defect_logs : set Defect
}
fact PhaseNamesAreUniqueWithinAProcess {
all p1 : Phase | all p2 : Phase - p1 | (p1.process = p2.process) implies (p1.name != p2.name)
}
fact NoTwoProcessesShareTheSamePhases {
all p1: Process | all p2 : Process - p1 | p1.phases & p2.phases = none
}
fact PhasesBelongToTheProcessThatIncludesThem {
all p : Phase | p in p.process.phases
}
fact PhaseTimeLogsPointBackToThePhaseItself {
all p : Phase | p.time_logs.phase = p
}
fact PhaseDefectLogsPointBackToThePhaseItself {
all p : Phase | p.defect_logs.phase = p
}
sig ProcessName {}
fact EveryProcessNameBelongsToSomeProcess {
all pn : ProcessName | some p : Process | p.name = pn
}
sig Process {
name : one ProcessName,
phases : some Phase
}
fact ProcessNamesAreUnique {
all p1: Process | all p2: Process - p1 | p1.name != p2.name
}
pred show {}
run show for 2 but 3 Phase
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.