edited a bit the sml function to adapt to the new data types

Author: AnoudAlshnakat

hol/bdd_test_casesScript.sml

@@ -20,22 +20,22 @@ open pred_specTheory;
 open policy_specTheory;   
 open tables_specTheory;
 open bdd_isomorphTheory;
-open bdd_end_to_endTheory;
-
-     
+open bdd_end_to_endTheory;     
 
 open policy_arith_to_varTheory;
 
+open table_arith_to_intervalTheory;
+
+
+     
 
 
 val _ = load "bdd_utils";   
 
 val _ = new_theory "bdd_test_cases";
 
-(* TODO: update the sml definition that takes a var bdd and generates var table, now the var_table has new syntax. Var x | True | False | Not atom --> 
-Var x | Not x | Not True | Not False | True | False
-
 
+    
 (* a few types abbreviations *)
 val _ = type_abbrev("BDD_tbl_type", “:(( (string# num list) var_table_list, (string# num list) action_expr) BDD)”);
 
@@ -79,7 +79,7 @@ val eval_policy1_full_opt_rhs = optionSyntax.dest_some (rhs (concl eval_policy1_
 
 (* automatically generate a table*)
 val test_groupings1 = rhs(concl(EVAL “[("a",["x";"y"]);("b",["z"])]”));
-val test_action_table1_auto =BDDUtils.bdd_to_tables_iterative eval_policy1_full_opt_rhs test_groupings1;
+val test_action_table1_auto = BDDUtils.bdd_to_tables_iterative eval_policy1_full_opt_rhs test_groupings1;
 
 (* now create a BDD for the table*)    
 val eval_table1_full_opt_auto = EVAL “mk_BDDPred_opt table_structure (0,[],[(0, non_termn (NONE, ^test_action_table1_auto))]) [] ["x";"y";"z"] 1”;
@@ -94,6 +94,19 @@ val policy1_thm_init = computeLib.RESTR_EVAL_CONV [“sem_tables”,“sem_polic
 val policy1_thm = SIMP_RULE bool_ss [correct_var_policy_var_tables_exec_thm1] policy1_thm_init;    
 
 
+(* from var tables to final single interval table*)
+
+
+
+   
+
+
+
+
+
+
+    
+
 (*    
 (* policy 1: var TABLE representation *)
 
@@ -301,6 +314,12 @@ val arith_policy3_var_policy3_thm = REWRITE_RULE[all_distinct_conj, arith_policy
 
 *)
 
-*)                       
+                      
 val _ = export_theory ();
 
+
+
+
+
+
+

hol/bdd_utils.sml

@@ -141,7 +141,7 @@ fun get_all_vars_in_group groupings group_name =
     | NONE => [];
 
 (* Generate action table for terminal nodes *)
-fun generate_action_table bdd_term =
+(*fun generate_action_table bdd_term =
     let
       val (start_state_term, rest) = dest_pair bdd_term
       val (edges_term, labelings_term) = dest_pair rest
@@ -172,6 +172,8 @@ fun generate_action_table bdd_term =
     in
       terminal_entries
     end;
+*)
+
 
 (* Enhanced find_paths_for_group that handles input states *)
 fun find_paths_for_group_with_inputs bdd_term groupings_term group_name input_states =
@@ -270,7 +272,7 @@ fun find_paths_for_group_with_inputs bdd_term groupings_term group_name input_st
           let
             val atom_vars = map (fn (var, value) =>
                   if value then ``Var ^(fromMLstring var)``
-                  else ``Not (Var ^(fromMLstring var))``
+                  else ``Not (^(fromMLstring var))``
               ) path
 
             val simplified_atoms =