/ - Diff - LustreC

« Previous | Next »

Revision 2f7c9195

Added by Pierre-Loïc Garoche over 5 years ago

ID 2f7c919514bae2ab404b92519591827763fa3828
Parent 3d3718ae
Child 4300981b

zustre progress. Issues with sliced predicates

     let check machines node =
       let machine = get_machine machines node in
       let node_id = machine.mname.node_id in
       (* Declaring collecting semantics *)
       let main_output =
         rename_machine_list machine.mname.node_id machine.mstep.step_outputs
         rename_machine_list node_id machine.mstep.step_outputs
       in
       let main_output_dummy =
         rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
         rename_machine_list ("dummy" ^ node_id) machine.mstep.step_outputs
       in
       let main_input =
         rename_machine_list machine.mname.node_id machine.mstep.step_inputs
         rename_machine_list node_id machine.mstep.step_inputs
       in
       let main_input_dummy =
         rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
         rename_machine_list ("dummy" ^ node_id) machine.mstep.step_inputs
       in
       let main_memory_next =
         main_input @ (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
-...
       (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
          Faut-il declarer les "rel" dans la hashtbl ?
       *)
       let decl_main = decl_rel "MAIN" main_memory_next in
       let decl_main =
         decl_rel
           ("MAIN" ^ "_" ^ node_id)
           (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
-...
         Z3.Expr.mk_app
           !ctx
           decl_main
           (List.map horn_var_to_expr main_memory_next)
           ((Z3.Arithmetic.Integer.mk_numeral_i !ctx 0)::(List.map horn_var_to_expr main_memory_next))
       in
       (* Special case when the main node is stateless *)
       let _ =
-...
       (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_current *)
       (*   step_name node *)
       (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
       let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in
       let k_var = decl_var k in
       let horn_head =
         Z3.Expr.mk_app
           !ctx
           decl_main
           (List.map horn_var_to_expr main_memory_next)
           ((Z3.Arithmetic.mk_add
     	  !ctx
     	  [Z3.Expr.mk_const_f !ctx k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
            )::(List.map horn_var_to_expr main_memory_next))
       in
       let horn_body =
         Z3.Boolean.mk_and !ctx
+          [
     	Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_current);
     	Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::(List.map horn_var_to_expr main_memory_current));
     	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
+          ]
       in
       (* Vars contains all vars: in_out, current, mid, neXt memories *)
       let vars = (step_vars_c_m_x machines machine) @ main_output_dummy @ main_input_dummy  in
       let _ =
         add_rule ~dont_touch:[decl_main] vars  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
         add_rule ~dont_touch:[decl_main] (k::vars)  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
       in
-...
       let not_prop =
         Z3.Boolean.mk_not !ctx prop
       in
       add_rule (*~dont_touch:[decl_main;decl_err]*) main_memory_next (Z3.Boolean.mk_implies !ctx
       add_rule (*~dont_touch:[decl_main;decl_err]*) (k::main_memory_next) (Z3.Boolean.mk_implies !ctx
+    	      (
     		Z3.Boolean.mk_and !ctx
     		  [not_prop;
     		   Z3.Expr.mk_app !ctx decl_main (List.map horn_var_to_expr main_memory_next);
     		   Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::List.map horn_var_to_expr main_memory_next);
+    		  ]
+    	      )
     	      (Z3.Expr.mk_app !ctx decl_err []))
-...
       Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status);
       match res_status with
       | Z3.Solver.SATISFIABLE -> (
          (*Zustre_cex.build_cex decl_err*)
         let expr1_opt = Z3.Fixedpoint.get_answer !fp in
         let expr2_opt = Z3.Fixedpoint.get_ground_sat_answer !fp in
            match expr1_opt, expr2_opt with
     	 None, None -> Format.eprintf "Sat No feedback@."
            | Some e, Some e2 -> Format.eprintf "Sat Result: %s, %s@."
     					   (Z3.Expr.to_string e)
     					   (Z3.Expr.to_string e2)
            | _ -> assert false
+      )
       | Z3.Solver.SATISFIABLE -> Zustre_cex.build_cex decl_err
       | Z3.Solver.UNSATISFIABLE -> (*build_inv*) (
            let expr_opt = Z3.Fixedpoint.get_answer !fp in
            match expr_opt with

       register_fdecl id.var_id fdecl;
       fdecl
     let decl_rel name args =
     let decl_rel name args_sorts =
       (*verifier ce qui est construit. On veut un declare-rel *)
       let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
       (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
       let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
       Z3.Fixedpoint.register_relation !fp fdecl;
       register_fdecl name fdecl;
-...
     	begin
     	  (* Declaring single predicate *)
     	  let vars = inout_vars machines m in
     	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars in
     	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
     	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
     	  let horn_body, _ (* don't care for reset here *) =
     	    instrs_to_expr
     	      machines
-...
     	  (* Rule for reset *)
     	  let vars = reset_vars machines m in
     	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars in
     	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
     	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
     	  let horn_reset_body = machine_reset machines m in
     	  let horn_reset_head =
     	    Z3.Expr.mk_app
-...
     	  (* Rule for step*)
     	  let vars = step_vars machines m in
               let _ = decl_rel (machine_step_name m.mname.node_id) vars in
       	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
               let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
     	  let horn_step_body, _ (* don't care for reset here *) =
     	    instrs_to_expr
     	      machines

Also available in: Unified diff

Project

General

Profile

CristalCaveGem » LustreC

Revision 2f7c9195

Added by Pierre-Loïc Garoche over 5 years ago