Property-based test for printer >> parser inverse, test excutable

lib/src/CoAlgLogics.ml

@@ -624,7 +624,7 @@ let oneStepSat_GML u sv =
   let (sort, v) = sv in
   let rels = bsetFold (fun lf accu -> let role = lfGetDest3 sort lf in role :: accu) v [] in
   let reled_v = List.map (fun rel -> (rel, bsetFilter v (fun lf -> lfGetDest3 sort lf = rel))) rels in
-  List.for_all (fun (rel, sub_v) ->
+  List.for_all (fun (_rel, sub_v) ->
       let counters = Hashtbl.create (bsetLen sub_v) in
       bsetIter (fun lf -> Hashtbl.add counters lf 0) v;
       oneStepGMLRec counters sort sub_v u

lib/tests/testsuite/cool_testsuite.ml

@@ -118,6 +118,8 @@ let gml_testcases =
     ; unsat "<10 a1>([8 a1]True | [7 a1]p8 <=> [0 a1]p3 & ~True)"
     ; unsat "<3 a1>~p & [0 a1]p"
     ; sat   "<3 a1>~p & [0 a2]p"
+    ; sat "<5 a1>~p & [2 a2]p"
+    ; sat "<0 a1>True & [0 a2]False"
     ]
 
 let pml_testcases =

lib/tests/unit_tests/CoAlgFormula_tests.ml

@@ -23,7 +23,14 @@ let treeParserAndSimplify_predicate formula =
 let treeParserAndSimplify_prop =
   "treeParserAndSimplify" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 ( make (sized Formula_gen.formula_K)) treeParserAndSimplify_predicate)
 
-let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop]
+let printAndParseInverse_predicate formula = 
+  importFormula (string_of_formula formula) = formula
+
+let printAndParseInverse_prop =
+  "printAndParseInverse" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 
+    (make (oneof [(sized Formula_gen.formula_GML); (sized Formula_gen.formula_CL)])) printAndParseInverse_predicate)
+
+let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop; "printAndParseInverse" >: printAndParseInverse_prop ]
                               
 
 (* vim: set et sw=2 sts=2 ts=8 : *)