basic implementation for abs report including witness plan
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)