chore: add VTS synthesis tool

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "engine/crates/pyo3-generic-wrap/example",
     "engine/crates/robust-diagnosis",
     "engine/crates/momba-simulator",
+    "engine/crates/vts-synth",
 ]
 exclude = ["private"]
 

engine/crates/vts-synth/.gitignore

@@ -0,0 +1 @@
+out

engine/crates/vts-synth/Cargo.toml

@@ -0,0 +1,28 @@
+[package]
+name = "vts-synth"
+description = "VTS synthesis tool."
+version = "0.1.0"
+edition = "2021"
+publish = false
+
+[features]
+disable-determinize = []
+disable-projection = []
+
+[dependencies]
+ariadne = "0.3"
+bit-set = "0.5"
+chumsky = "0.9"
+clap = { version = "4.4", features = ["derive"] }
+cudd-sys = "1.0"
+hashbrown = { version = "0.14", features = ["raw"] }
+im = "15.1"
+indexmap = { version = "2.0", features = ["serde"] }
+quick-xml = { version = "0.34", features = ["serialize"] }
+rand = "0.8"
+serde = { version = "1.0", features = ["derive", "rc"] }
+serde_json = "1.0"
+serde_yaml = "0.9"
+thiserror = "1.0"
+tracing = { version = "0.1.37", features = ["release_max_level_info"] }
+tracing-subscriber = "0.3.17"

engine/crates/vts-synth/models/coffee-machine.fm

@@ -0,0 +1 @@
+true

engine/crates/vts-synth/models/coffee-machine.fts.xml

@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<fts:fts xmlns:fts="http://www.unamur.be/xml/fts/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+    <fts:start>idle</fts:start>
+    <fts:states>
+        <fts:state id="idle">
+            <fts:transition action="espresso" target="dispense" />
+            <fts:transition action="cappuccino" target="dispense" />
+        </fts:state>
+        <fts:state id="dispense">
+            <fts:transition action="dispense" target="idle" />
+            <fts:transition action="pump_fault" fexpression="PumpFault" target="pump_fault" />
+            <fts:transition action="short_circuit" fexpression="ShortCircuit" target="short_circuit" />
+        </fts:state>
+        <fts:state id="pump_fault">
+            <fts:transition action="espresso" target="pump_fault" />
+            <fts:transition action="cappuccino" target="pump_fault" />
+        </fts:state>
+        <fts:state id="short_circuit">
+            <fts:transition action="burn" target="short_circuit" />
+        </fts:state>
+    </fts:states>
+</fts:fts>

engine/crates/vts-synth/models/coffee-machine2.fts.xml

@@ -0,0 +1,23 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<fts:fts xmlns:fts="http://www.unamur.be/xml/fts/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+    <fts:start>idle</fts:start>
+    <fts:states>
+        <fts:state id="idle">
+            <fts:transition action="espresso" target="dispense" />
+            <fts:transition action="cappuccino" target="dispense" />
+        </fts:state>
+        <fts:state id="dispense">
+            <fts:transition action="dispense" target="idle" />
+            <fts:transition action="pump_fault" fexpression="PumpFault" target="pump_fault" />
+            <fts:transition action="short_circuit" fexpression="ShortCircuit" target="short_circuit" />
+        </fts:state>
+        <fts:state id="pump_fault">
+            <fts:transition action="espresso" target="pump_fault" />
+            <fts:transition action="cappuccino" target="pump_fault" />
+            <fts:transition action="short_circuit" fexpression="ShortCircuit" target="short_circuit" />
+        </fts:state>
+        <fts:state id="short_circuit">
+            <fts:transition action="burn" target="short_circuit" />
+        </fts:state>
+    </fts:states>
+</fts:fts>

engine/crates/vts-synth/models/email.fm

@@ -0,0 +1 @@
+(s && !e) || (e && !s) || (s && e)

engine/crates/vts-synth/models/email.fts.xml

@@ -0,0 +1,17 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<fts:fts xmlns:fts="http://www.unamur.be/xml/fts/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+    <fts:start>idle</fts:start>
+    <fts:states>
+        <fts:state id="idle">
+            <fts:transition action="sign" target="signed" fexpression="s" />
+            <fts:transition action="enc" target="encrypted" fexpression="e &amp;&amp; !s" />
+        </fts:state>
+        <fts:state id="signed">
+            <fts:transition action="send" target="idle" fexpression="s &amp;&amp; !e" />
+            <fts:transition action="enc" target="encrypted" fexpression="e" />
+        </fts:state>
+        <fts:state id="encrypted">
+            <fts:transition action="send" target="idle" />
+        </fts:state>
+    </fts:states>
+</fts:fts>

engine/crates/vts-synth/models/simple.fts.xml

@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<fts:fts xmlns:fts="http://www.unamur.be/xml/fts/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
+    <fts:start>s1</fts:start>
+    <fts:states>
+        <fts:state id="s1">
+            <fts:transition fexpression="Fa" target="s2" />
+            <fts:transition fexpression="Fb" target="s3" />
+        </fts:state>
+        <fts:state id="s2">
+            <fts:transition action="a" target="s4" />
+            <fts:transition action="a" target="s5" />
+        </fts:state>
+        <fts:state id="s3">
+            <fts:transition action="b" target="s5" />
+        </fts:state>
+        <fts:state id="s4">
+            <fts:transition target="s6" />
+        </fts:state>
+        <fts:state id="s5">
+            <fts:transition action="c" fexpression="Fc" target="s5" />
+        </fts:state>
+        <fts:state id="s6">
+            <fts:transition target="s7" />
+        </fts:state>
+        <fts:state id="s7">
+            <fts:transition action="c" fexpression="Fc" target="s4" />
+        </fts:state>
+    </fts:states>
+</fts:fts>

engine/crates/vts-synth/models/vibes/README.md

@@ -0,0 +1,9 @@
+# VIBeS FTS Models
+
+The models in this directory are from the [VIBeS project](https://projects.info.unamur.be/vibes/index.html) of [UNamur](https://www.unamur.be/en/).
+
+- [Aero UC5](https://projects.info.unamur.be/vibes/case-study-aerouc5.html) ([`aerouc5.fts.xml`](aerouc5.fts.xml))
+- [Soda Vending Machine](https://projects.info.unamur.be/vibes/case-study-svm.html) ([`svm.fts.xml`](svm.fts.xml))
+- [Claroline](https://projects.info.unamur.be/vibes/case-study-claroline.html) ([`claroline-pow.fts.xml`](claroline-pow.fts.xml))
+- [Card Payment Terminal](https://projects.info.unamur.be/vibes/case-study-cpterminal.html) ([`cpterminal.fts.xml`](cpterminal.fts.xml))
+- [Minepump](https://projects.info.unamur.be/vibes/case-study-minepump.html) ([`minepump.fts.xml`](minepump.fts.xml))

engine/crates/vts-synth/models/vibes/aerouc5.fm

@@ -0,0 +1 @@
+(!Check_for_obstacles || OWS) && (!Mark_landing_position || HMS_D) && (!Mark_landing_position || HOCAS) && (!Display_real_reference_objects || OWS) && (!SI_sensor_based || OWS) && (!SI_from_DB || Database) && (!Provide_slope_indication_for_LP || Mark_landing_position) && (!AeroUc5 || HOCAS) && (!AeroUc5 || Mark_landing_position) && (!AeroUc5 || Database) && (!AeroUc5 || HMS_D) && (!AeroUc5 || OWS) && (!AeroUc5 || Display_reference_objects_in_landing_zone) && (!AeroUc5 || Provide_slope_indication_for_LP) && (HOCAS_GE_Aviation_Systems || x29 || !HOCAS) && (HOCAS_Honeywell || !x29 || !HOCAS) && (!HOCAS_GE_Aviation_Systems || x30 || !HOCAS) && (!HOCAS_Honeywell || !x30 || !HOCAS) && (!HOCAS_GE_Aviation_Systems || HOCAS) && (!HOCAS_Honeywell || HOCAS) && (!HOCAS || AeroUc5) && (!Mark_landing_position || Mark_LP) && (!Mark_landing_position || ArtificialParentCheck_for_obstacles) && (!Mark_landing_position || Check_for_no_ground) && (Mark_LP_by_handling_pilot_only || x31 || !Mark_LP) && (Mark_LP_by_both_pilots || !x31 || !Mark_LP) && (!Mark_LP_by_handling_pilot_only || x32 || !Mark_LP) && (!Mark_LP_by_both_pilots || !x32 || !Mark_LP) && (!Mark_LP_by_handling_pilot_only || Mark_LP) && (!Mark_LP_by_both_pilots || Mark_LP) && (!Mark_LP || Mark_landing_position) && (!Check_for_obstacles || ArtificialParentCheck_for_obstacles) && (!ArtificialParentCheck_for_obstacles || Mark_landing_position) && (!Check_for_no_ground || Mark_landing_position) && (!Mark_landing_position || AeroUc5) && (DB_provided_by_customer || x33 || !Database) && (DB_provided_by_Cassidian || !x33 || !Database) && (!DB_provided_by_customer || x34 || !Database) && (!DB_provided_by_Cassidian || !x34 || !Database) && (!DB_provided_by_customer || Database) && (!DB_provided_by_Cassidian || Database) && (!Database || AeroUc5) && (HMS_D_Elbit || x35 || !HMS_D) && (HMS_D_Thales || !x35 || !HMS_D) && (!HMS_D_Elbit || x36 || !HMS_D) && (!HMS_D_Thales || !x36 || !HMS_D) && (!HMS_D_Elbit || HMS_D) && (!HMS_D_Thales || HMS_D) && (!HMS_D || AeroUc5) && (HELLAS || x37 || !OWS) && (ELOP || !x37 || !OWS) && (!HELLAS || x38 || !OWS) && (!ELOP || !x38 || !OWS) && (!HELLAS || OWS) && (!ELOP || OWS) && (!OWS || AeroUc5) && (!Display_reference_objects_in_landing_zone || ArtificialParentDisplay_real_reference_objects) && (!Display_reference_objects_in_landing_zone || Display_visual_3D_cues) && (!Display_real_reference_objects || ArtificialParentDisplay_real_reference_objects) && (!ArtificialParentDisplay_real_reference_objects || Display_reference_objects_in_landing_zone) && (!Display_visual_3D_cues || Display_reference_objects_in_landing_zone) && (!Display_reference_objects_in_landing_zone || AeroUc5) && (SI_sensor_based || x39 || !Provide_slope_indication_for_LP) && (SI_from_DB || !x39 || !Provide_slope_indication_for_LP) && (!SI_sensor_based || x40 || !Provide_slope_indication_for_LP) && (!SI_from_DB || !x40 || !Provide_slope_indication_for_LP) && (!SI_sensor_based || Provide_slope_indication_for_LP) && (!SI_from_DB || Provide_slope_indication_for_LP) && (!Provide_slope_indication_for_LP || AeroUc5) && (AeroUc5)

engine/crates/vts-synth/models/vibes/aerouc5.fts.xml

@@ -0,0 +1,101 @@
+<?xml version="1.0"?><fts>
+    <start>s0</start>
+    <states>
+        <state id="s99">
+            <transition target="s0"></transition>
+        </state>
+        <state id="Approach_line_landing_doghouse_and_reference_objects_displayed_end">
+            <transition target="symbology_is_displayed_end"></transition>
+            <transition target="Approach_line_takeoff_doghouse_and_reference_objects_displayed_start" action="Landing_and_touchdown_for_more_than_5_sec"></transition>
+            <transition target="S5"></transition>
+            <transition target="Pin_with_slope_indication_approach_line_landing_doghouse_displayed" action="Depart_from_landing_position"></transition>
+        </state>
+        <state id="landing_position_is_marked_start">
+            <transition target="S21"></transition>
+        </state>
+        <state id="Approach_line_takeoff_doghouse_and_real_objects_displayed">
+            <transition target="Approach_line_takeoff_doghouse_and_reference_objects_displayed_end"></transition>
+        </state>
+        <state id="Approach_line_landing_doghouse_and_reference_objects_displayed_start">
+            <transition target="Approach_line_landing_doghouse_and_virtual_3D_cues_displayed" action="Virtual_3D_cues_displayed" fexpression="Display_visual_3D_cues"></transition>
+            <transition target="Approach_line_landing_doghouse_and_real_objects_displayed" action="Real_objects_displayed" fexpression="Display_real_reference_objects"></transition>
+        </state>
+        <state id="Pin_and_approach_line_displayed">
+            <transition target="Pin_with_slope_indication_and_approach_line_displayed" action="Approach_to_landing_position"></transition>
+            <transition target="Pin_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="S5" action="Approach_to_landing_position"></transition>
+        </state>
+        <state id="symbology_is_displayed_start">
+            <transition target="Pin_displayed" action="Approach_to_landing_position"></transition>
+        </state>
+        <state id="NO_Ground_displayed">
+            <transition target="S21"></transition>
+        </state>
+        <state id="Approach_line_landing_doghouse_and_virtual_3D_cues_displayed">
+            <transition target="Approach_line_landing_doghouse_and_reference_objects_displayed_end"></transition>
+        </state>
+        <state id="Pin_displayed">
+            <transition target="S5" action="Approach_to_landing_position"></transition>
+            <transition target="Pin_and_approach_line_displayed" action="Approach_to_landing_position"></transition>
+        </state>
+        <state id="Landing_Position_is_marked">
+            <transition target="NO_Ground_displayed" action="Provide_landing_position_not_on_ground" fexpression="Check_for_no_ground"></transition>
+            <transition target="displayed" action="Provide_landing_position_with_obstacle" fexpression="Check_for_obstacles"></transition>
+            <transition target="landing_position_is_marked_end" action="Provide_valid_landing_position"></transition>
+        </state>
+        <state id="Pin_with_slope_indication_approach_line_landing_doghouse_displayed">
+            <transition target="Approach_line_landing_doghouse_and_reference_objects_displayed_start" action="Approach_to_landing_position"></transition>
+            <transition target="Pin_with_slope_indication_and_approach_line_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="S5"></transition>
+        </state>
+        <state id="Approach_line_landing_doghouse_and_real_objects_displayed">
+            <transition target="Approach_line_landing_doghouse_and_reference_objects_displayed_end"></transition>
+        </state>
+        <state id="s0">
+            <transition target="standby" action="activate"></transition>
+        </state>
+        <state id="landing_position_is_marked_end">
+            <transition target="symbology_is_displayed_start"></transition>
+        </state>
+        <state id="Approach_line_takeoff_doghouse_and_reference_objects_displayed_start">
+            <transition target="Approach_line_takeoff_doghouse_and_virtual_3D_cues_displayed" action="Virtual_3D_cues_displayed" fexpression="Display_visual_3D_cues"></transition>
+            <transition target="Approach_line_takeoff_doghouse_and_real_objects_displayed" action="Real_objects_displayed" fexpression="Display_real_reference_objects"></transition>
+        </state>
+        <state id="S21">
+            <transition target="Landing_Position_is_marked" action="Trigger_mark_landing_position"></transition>
+        </state>
+        <state id="Pin_with_slope_indication_and_approach_line_displayed">
+            <transition target="Pin_with_slope_indication_approach_line_landing_doghouse_displayed" action="Approach_to_landing_position"></transition>
+            <transition target="S5"></transition>
+            <transition target="Pin_and_approach_line_displayed" action="Depart_from_landing_position"></transition>
+        </state>
+        <state id="S5">
+            <transition target="Pin_with_slope_indication_approach_line_landing_doghouse_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="Pin_and_approach_line_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="Pin_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="Pin_with_slope_indication_and_approach_line_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="Approach_line_landing_doghouse_and_reference_objects_displayed_start" action="Approach_to_landing_position"></transition>
+            <transition target="Approach_line_takeoff_doghouse_and_reference_objects_displayed_start" action="Landing_and_touchdown_for_more_than_5_sec"></transition>
+        </state>
+        <state id="symbology_is_displayed_end">
+            <transition target="s99" action="deactivate"></transition>
+        </state>
+        <state id="displayed">
+            <transition target="S21"></transition>
+        </state>
+        <state id="standby">
+            <transition target="landing_position_is_marked_start"></transition>
+        </state>
+        <state id="Approach_line_takeoff_doghouse_and_reference_objects_displayed_end">
+            <transition target="Approach_line_and_takeoff_doghouse_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="S5"></transition>
+        </state>
+        <state id="Approach_line_and_takeoff_doghouse_displayed">
+            <transition target="Pin_with_slope_indication_approach_line_landing_doghouse_displayed" action="Depart_from_landing_position"></transition>
+            <transition target="S5"></transition>
+        </state>
+        <state id="Approach_line_takeoff_doghouse_and_virtual_3D_cues_displayed">
+            <transition target="Approach_line_takeoff_doghouse_and_reference_objects_displayed_end"></transition>
+        </state>
+    </states>
+</fts>

engine/crates/vts-synth/models/vibes/aerouc5.out

@@ -0,0 +1,57 @@
+Features: {"Display_visual_3D_cues", "Display_real_reference_objects", "Check_for_no_ground", "Check_for_obstacles", "OWS", "Mark_landing_position", "HMS_D", "HOCAS", "SI_sensor_based", "SI_from_DB", "Database", "Provide_slope_indication_for_LP", "AeroUc5", "Display_reference_objects_in_landing_zone", "HOCAS_GE_Aviation_Systems", "x29", "HOCAS_Honeywell", "x30", "Mark_LP", "ArtificialParentCheck_for_obstacles", "Mark_LP_by_handling_pilot_only", "x31", "Mark_LP_by_both_pilots", "x32", "DB_provided_by_customer", "x33", "DB_provided_by_Cassidian", "x34", "HMS_D_Elbit", "x35", "HMS_D_Thales", "x36", "HELLAS", "x37", "ELOP", "x38", "ArtificialParentDisplay_real_reference_objects", "x39", "x40"}
+Observables: {"activate", "Landing_and_touchdown_for_more_than_5_sec", "Depart_from_landing_position", "deactivate", "Virtual_3D_cues_displayed", "Real_objects_displayed", "Approach_to_landing_position", "Trigger_mark_landing_position", "Provide_landing_position_not_on_ground", "Provide_landing_position_with_obstacle", "Provide_valid_landing_position"}
+
+States: 25 (initial: 1)
+Transitions: 46
+SCCs: 1
+
+== Initial VTS ==
+States: 108 (initial: 1)
+Transitions: 208
+SCCs: 14
+Deterministic: false
+Monotonic: true
+
+== Refined VTS ==
+States: 106 (initial: 1)
+Transitions: 204
+SCCs: 12
+Deterministic: false
+Monotonic: true
+
+== Observability Projection ==
+States: 75 (initial: 1)
+Transitions: 280
+SCCs: 9
+Deterministic: false
+Monotonic: true
+
+== Determinize ==
+States: 85 (initial: 1)
+Transitions: 241
+SCCs: 12
+
+== Flatten Beliefs ==
+States: 85 (initial: 1)
+Transitions: 241
+SCCs: 12
+Deterministic: true
+Monotonic: true
+
+== Compress SCCs ==
+States: 48 (initial: 1)
+Transitions: 152
+SCCs: 12
+Deterministic: true
+Monotonic: true
+
+== Compress Transitions ==
+States: 45 (initial: 1)
+Transitions: 152
+SCCs: 11
+Deterministic: true
+Monotonic: true
+
+real    0m0.126s
+user    0m0.090s
+sys     0m0.041s