Alloy model of PSP data model

cartographer_data_model.als

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