[lustresf] add Program constructor in model examples + sf_sem

src/tools/stateflow/common/datatype.ml

@@ -83,7 +83,7 @@ struct
 
   let init_env model = ActiveStates.Env.from_set (states model) false
 
-  let global_vars (_, _, env) = env
+  let global_vars (Program (_, _, env)) = env
 
   (* Printers *)
 

src/tools/stateflow/models/model_medium.ml

@@ -4,7 +4,7 @@ open SF
 let name = "medium"
 
 let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
- 
+
 let model : prog_t =
     let state_main = "main" in
     let state_a = "a" in
@@ -85,6 +85,6 @@ let model : prog_t =
 	       Junction("jmid", [tB]);
 	      ]
     in
-    (state_main, src, [])
+    Program (state_main, src, [])
 
 let traces : trace_t list = [[None; None]]

src/tools/stateflow/models/model_simple.ml

@@ -5,7 +5,7 @@ let name = "simple"
 
   let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
   let action _ = no_action
- 
+
 let model : prog_t =
     let state_main = "main" in
     let state_a = "a" in
@@ -77,6 +77,6 @@ let model : prog_t =
 	       State([state_main], def_main);
 	      ]
     in
-    (state_main, src, [])
+    Program (state_main, src, [])
 
 let traces : trace_t list = [[None; None]]

src/tools/stateflow/models/model_stopwatch.ml

@@ -6,10 +6,10 @@ let verbose = false
 let actionv x = no_action (*TODO if verbose then action x else no_action*)
 let action x = no_action (* TODO *)
 let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
-    
+
 let name = "stopwatch"
-  
-let model = 
+
+let model =
   let smain    = "main" in
   let sstop    = "stop" in
   let sreset   = "reset" in
@@ -53,7 +53,7 @@ let model =
     dest = DPath [smain;srun;srunning];
   }
   in
-  
+
   let tlapstop_lap  = {
     event = event "LAP";
     condition = no_condition;
@@ -259,7 +259,7 @@ let model =
        "cont"
       ]
   in
-  (smain, src, globals)
+  Program (smain, src, globals)
 
 let traces : trace_t list =
   [