Functional.mch

/*
 * This file was generated by B4MSecure on Wednesday, November 22, 2023 at 3:14:53 PM CET
 * -
 * B4MSecure Eclipse IDE Integration (part of B4MSecure) version 2.0.5.202104011214
 * Please visit http://b4msecure.forge.imag.fr for further information
 */


MACHINE 
	
	Functional

DEFINITIONS
	"Functional.def"

SETS
	
	PATIENT = {p1, p2, p3} ;
    MEDICALRECORD = {m1, m2, m3}

ABSTRACT_VARIABLES
	
	Patient,
	MedicalRecord,
	mRecords,
	MedicalRecord_data,
	MedicalRecord_valid

INVARIANT
	
	Patient : FIN(PATIENT) &
	MedicalRecord : FIN(MEDICALRECORD) &
	mRecords : MedicalRecord +-> Patient &
	MedicalRecord_data : MedicalRecord +-> STRING &
	MedicalRecord_valid : MedicalRecord --> BOOL &
	
	/* 
	 * InvalidRecordConstraint [Defined in Package HospitalSystem::Functional]
	 */
	!(p).(p : Patient => card(( mRecords~[{p}] <| MedicalRecord_valid) |> {FALSE}) <= 1)

INITIALISATION
	
	Patient := {} ||
	MedicalRecord := {} ||
	mRecords := {} ||
	MedicalRecord_data := {} ||
	MedicalRecord_valid := {}

OPERATIONS
	
	MedicalRecord_validate(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord &
		/* 
		 * pre-condition [Defined in Operation HospitalSystem::Functional::MedicalRecord::validate]
		 */
		MedicalRecord_valid(aMedicalRecord) = FALSE
		
	THEN 
		/* 
		 * body [Defined in Operation HospitalSystem::Functional::MedicalRecord::validate]
		 */
		MedicalRecord_valid(aMedicalRecord) := TRUE
	END;

	Patient_NEW(aPatient) = 
	PRE	aPatient : PATIENT &
		aPatient /: Patient
		
	THEN 
		Patient := Patient \/ {aPatient}
	END;

	MedicalRecord_NEW(aMedicalRecord) = 
	PRE	aMedicalRecord : MEDICALRECORD &
		aMedicalRecord /: MedicalRecord
		
	THEN 
		MedicalRecord := MedicalRecord \/ {aMedicalRecord} ||
		MedicalRecord_valid := MedicalRecord_valid \/ {(aMedicalRecord |-> FALSE)}
	END;

	Patient_Free(aPatient) = 
	PRE	aPatient : Patient
		
	THEN 
		Patient := Patient - {aPatient} ||
		mRecords := mRecords |>> {aPatient}
	END;

	MedicalRecord_Free(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord
		
	THEN 
		MedicalRecord := MedicalRecord - {aMedicalRecord} ||
		mRecords := {aMedicalRecord} <<| mRecords ||
		MedicalRecord_data := {aMedicalRecord} <<| MedicalRecord_data ||
		MedicalRecord_valid := {aMedicalRecord} <<| MedicalRecord_valid
	END;

	result <-- MedicalRecord_GetPatient(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord &
		aMedicalRecord : dom(mRecords)
		
	THEN 
		result := MedicalRecord_patient(aMedicalRecord)
	END;

	result <-- Patient_GetMedicalrecord(aPatient) = 
	PRE	aPatient : Patient &
		aPatient : ran(mRecords)
		
	THEN 
		result := Patient_medicalrecord[{aPatient}]
	END;

	MedicalRecord_SetPatient(aMedicalRecord,aPatient) = 
	PRE	aMedicalRecord : MedicalRecord &
		aPatient : Patient &
		{(aMedicalRecord |-> aPatient)} /<: mRecords
		
	THEN 
		mRecords := ({aMedicalRecord} <<| mRecords) \/ {(aMedicalRecord |-> aPatient)}
	END;

	Patient_SetMedicalrecord(aPatient,theMedicalrecord) = 
	PRE	aPatient : Patient &
		theMedicalrecord : FIN(MedicalRecord) &
		(theMedicalrecord * {aPatient}) /<: mRecords &
		!added.( added : theMedicalrecord => MedicalRecord_patient[{added}] = {})
		
	THEN 
		mRecords := (mRecords |>> {aPatient}) \/ (theMedicalrecord * {aPatient})
	END;

	MedicalRecord_UnsetPatient(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord
		
	THEN 
		mRecords := {aMedicalRecord} <<| mRecords
	END;

	Patient_UnsetMedicalrecord(aPatient) = 
	PRE	aPatient : Patient
		
	THEN 
		mRecords := mRecords |>> {aPatient}
	END;

	Patient_AddMedicalrecord(aPatient,aMedicalrecord) = 
	PRE	aPatient : Patient &
		aMedicalrecord : MedicalRecord &
		(aMedicalrecord |-> aPatient) /: mRecords &
		MedicalRecord_patient[{aMedicalrecord}] = {}
		
	THEN 
		mRecords := mRecords \/ {(aMedicalrecord |-> aPatient)}
	END;

	MedicalRecord_RemovePatient(aMedicalRecord,aPatient) = 
	PRE	aMedicalRecord : MedicalRecord &
		aPatient : Patient &
		(aMedicalRecord |-> aPatient) : mRecords
		
	THEN 
		mRecords := mRecords - {(aMedicalRecord |-> aPatient)}
	END;

	Patient_RemoveMedicalrecord(aPatient,aMedicalrecord) = 
	PRE	aPatient : Patient &
		aMedicalrecord : MedicalRecord &
		(aMedicalrecord |-> aPatient) : mRecords
		
	THEN 
		mRecords := mRecords - {(aMedicalrecord |-> aPatient)}
	END;

	result <-- MedicalRecord_GetData(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord &
		aMedicalRecord : dom(MedicalRecord_data)
		
	THEN 
		result := MedicalRecord_data(aMedicalRecord)
	END;

	result <-- MedicalRecord_GetValid(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord &
		aMedicalRecord : dom(MedicalRecord_valid)
		
	THEN 
		result := MedicalRecord_valid(aMedicalRecord)
	END;

	MedicalRecord_SetData(aMedicalRecord,aData) = 
	PRE	aMedicalRecord : MedicalRecord &
		aData : STRING
		
	THEN 
		MedicalRecord_data := ({aMedicalRecord} <<| MedicalRecord_data)  \/ {(aMedicalRecord |-> aData)}
	END;

	MedicalRecord_SetValid(aMedicalRecord,aValid) = 
	PRE	aMedicalRecord : MedicalRecord &
		aValid : BOOL
		
	THEN 
		MedicalRecord_valid := ({aMedicalRecord} <<| MedicalRecord_valid)  \/ {(aMedicalRecord |-> aValid)}
	END;

	MedicalRecord_UnsetData(aMedicalRecord) = 
	PRE	aMedicalRecord : MedicalRecord
		
	THEN 
		MedicalRecord_data := {aMedicalRecord} <<| MedicalRecord_data
	END;

	MedicalRecord_RemoveData(aMedicalRecord,aData) = 
	PRE	aMedicalRecord : MedicalRecord &
		aData : STRING &
		{(aMedicalRecord |-> aData)} <: MedicalRecord_data
		
	THEN 
		MedicalRecord_data := MedicalRecord_data - {(aMedicalRecord |-> aData)}
	END


END