diff options
Diffstat (limited to '')
| -rw-r--r-- | test/test_embedding.ml | 5 | ||||
| -rw-r--r-- | test/test_vm.ml | 54 |
2 files changed, 53 insertions, 6 deletions
diff --git a/test/test_embedding.ml b/test/test_embedding.ml index ea55e4f..a2eab95 100644 --- a/test/test_embedding.ml +++ b/test/test_embedding.ml @@ -66,9 +66,12 @@ let test_kernel_scan () = | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error let test_kernel_totality () = + (* A universal over an infinite domain whose body the symbolic + fragment cannot read: neither enumerable nor provable, so it + must be rejected, embedding or not. *) match solve - {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} + {| [ForAll variable: X quantifier: [Integer value: X] body: [Sensor id: X]] |} with | Error (Sol.Vm.Non_total_plan _) -> () | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard" diff --git a/test/test_vm.ml b/test/test_vm.ml index f3d8484..16ca63c 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -263,13 +263,47 @@ let test_forall_fails () = | [ _ :: _ ] -> Alcotest.fail "the universal must fail: Ana is 12" | _ -> Alcotest.fail "expected one query" -let test_forall_over_infinite_rejected () = - match load {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} with +let holds source = count_solutions source = 1 + +(* Symbolic discharge: the specification's own two examples, decided + without enumerating anything. *) + +let test_symbolic_naturals_nonnegative () = + Alcotest.(check bool) "every natural is at least zero" true + (holds + {| Query expression: [ForAll variable: X quantifier: [Natural value: X] body: [GreaterEqual left: X right: 0]] |}) + +let test_symbolic_integers_not_nonnegative () = + Alcotest.(check bool) "not every integer is at least zero" false + (holds + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [GreaterEqual left: X right: 0]] |}) + +let test_symbolic_inclusion () = + (* Decision 12: subtype inclusion, decided symbolically. *) + Alcotest.(check bool) "every integer is a rational" true + (holds + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Rational value: X]] |}); + Alcotest.(check bool) "not every rational is an integer" false + (holds + {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Integer value: X]] |}) + +let test_symbolic_interval_entailment () = + Alcotest.(check bool) "naturals from ten upward exceed five" true + (holds + {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |}) + +let test_forall_outside_fragment_still_rejected () = + match + load + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Equal left: X right: 5]] |} + with | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error | Ok (world, [ query ]) -> ( match Sol.Vm.Standalone.solve world query with | Error (Sol.Vm.Non_total_plan _) -> () - | Ok _ -> Alcotest.fail "a universal over an infinite domain must be rejected") + | Ok _ -> + Alcotest.fail + "a universal the symbolic fragment cannot read must still be rejected") | Ok _ -> Alcotest.fail "expected one query" let test_exists () = @@ -444,10 +478,20 @@ let () = [ Alcotest.test_case "forall holds" `Quick test_forall_holds; Alcotest.test_case "forall fails" `Quick test_forall_fails; - Alcotest.test_case "forall over infinite rejected" `Quick - test_forall_over_infinite_rejected; Alcotest.test_case "exists" `Quick test_exists; ] ); + ( "symbolic", + [ + Alcotest.test_case "naturals nonnegative" `Quick + test_symbolic_naturals_nonnegative; + Alcotest.test_case "integers not nonnegative" `Quick + test_symbolic_integers_not_nonnegative; + Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion; + Alcotest.test_case "interval entailment" `Quick + test_symbolic_interval_entailment; + Alcotest.test_case "outside fragment still rejected" `Quick + test_forall_outside_fragment_still_rejected; + ] ); ( "criteria", [ Alcotest.test_case "criterion admits" `Quick test_criterion_admits; |