Mentions légales du service

Skip to content

basic implementation for abs report including witness plan

Vojtisek Didier requested to merge 148-add-an-absreporting-model into master

This MR provides an xtex editor (and underlying ecore) for .absreport files This kind of file can store some witness plan connected to the original goal, and abs definitions

example for a small abs inspired from building (cf. fr/irisa/atsyra/absreport/tests/ABSReportMiniZonesTest)

one can write/read the following absreport (using full qualified name to elements in the abs file)

goal ThreeZones_system_goals.can_reach_Z3_from_Z1 {
	witness {
		metadata {
			duration 10
			timestamp "2022-02-14 12:00"
			rawCommand "its-reach ...."
		}
		steps {
			Building_behavior_def.open_door ( ThreeZones_system.Attacker1, ThreeZones_system.Z1_to_Z2)
			Building_behavior_def.goes_from_to_via (ThreeZones_system.Attacker1 , ThreeZones_system.Z1 , ThreeZones_system.Z2, ThreeZones_system.Z1_to_Z2)
			Building_behavior_def.open_door ( ThreeZones_system.Attacker1, ThreeZones_system.Z2_to_Z3)
			Building_behavior_def.goes_from_to_via( ThreeZones_system.Attacker1, ThreeZones_system.Z2, ThreeZones_system.Z3, ThreeZones_system.Z2_to_Z3)
		}
		initialState {
			ThreeZones_system.Attacker1{Building_behavior_def.location = ThreeZones_system.Z1}
		}
		finalState {
			ThreeZones_system.Attacker1{Building_behavior_def.location= ThreeZones_system.Z3},
			ThreeZones_system.Z1_to_Z2{Building_behavior_def.isOpen= true},
			ThreeZones_system.Z2_to_Z3{Building_behavior_def.isOpen= true}
		}
	}
}

It currently stores only the initial and final states.

We consider that default values are optional (ie. no need to write ThreeZones_system.Z1_to_Z2{Building_behavior_def.isOpen= false}, ThreeZones_system.Z2_to_Z3{Building_behavior_def.isOpen= false} in the initial state)

Closes #148 (closed) Closes #162 (closed)

Merge request reports