From 32b7d699152d70845196706e966b9bf49a0066e6 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Mon, 12 Feb 2024 16:31:36 +0100 Subject: [PATCH] [WIP] Add a runtime for qcheck-stm The runtime reimplement the QCheckSTM.Sequential.Make functor to use new postcond function --- dune-project | 18 + examples/lwt_dllist_tests.ml | 678 +++++--- examples/varray_circular_tests.ml | 1503 ++++++++++++----- examples/varray_tests.ml | 1485 +++++++++++----- ortac-runtime-qcheck-stm.opam | 40 + plugins/qcheck-stm/src/runtime/dune | 10 + .../src/runtime/ortac_runtime_qcheck_stm.ml | 75 + plugins/qcheck-stm/src/stm_of_ir.ml | 20 +- .../test/array_stm_tests.expected.ml | 887 +++++++--- .../conjunctive_clauses_stm_tests.expected.ml | 174 +- plugins/qcheck-stm/test/dune.inc | 14 +- plugins/qcheck-stm/test/dune_gen.ml | 2 +- .../test/hashtbl_stm_tests.expected.ml | 514 +++--- .../test/invariants_stm_tests.expected.ml | 100 +- .../test/record_stm_tests.expected.ml | 245 ++- .../qcheck-stm/test/ref_stm_tests.expected.ml | 96 +- .../test/sequence_model_stm_tests.expected.ml | 32 +- src/runtime/ortac_runtime_intf.ml | 1 + 18 files changed, 4101 insertions(+), 1793 deletions(-) create mode 100644 ortac-runtime-qcheck-stm.opam create mode 100644 plugins/qcheck-stm/src/runtime/dune create mode 100644 plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml diff --git a/dune-project b/dune-project index c10118b4..adc96ac2 100644 --- a/dune-project +++ b/dune-project @@ -164,6 +164,24 @@ (conflicts (result (< 1.5)))) +(package + (name ortac-runtime-qcheck-stm) + (synopsis "Runtime support library for Ortac/QCheck-STM-generated code") + (description + "\> The ortac-runtime-qcheck-stm library provides support for the code + "\> generated by the Ortac/QCheck-STM plugin (provided by the + "\> ortac-qcheck-stm package). + "\> + "\> Ortac (OCaml Runtime Assertion Checking) is a tool to turn + "\> executable Gospel specifications into code to test they hold. + ) + (authors "Nicolas Osborne ") + (maintainers "Nicolas Osborne ") + (depends + (ocaml (>= 4.11.0)) + qcheck-stm + ortac-runtime)) + (package (name ortac-examples) (synopsis diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml index fdbccdf2..e4afe376 100644 --- a/examples/lwt_dllist_tests.ml +++ b/examples/lwt_dllist_tests.ml @@ -1,8 +1,9 @@ +[@@@ocaml.warning "-26-27"] open Lwt_dllist_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Lwt_dllist_incl type sut = int t type cmd = @@ -282,254 +283,7 @@ module Spec = | Take_r -> true | Take_opt_l -> true | Take_opt_r -> true - let postcond cmd__005_ state__006_ res__007_ = - let new_state__008_ = lazy (next_state cmd__005_ state__006_) in - match (cmd__005_, res__007_) with - | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__008_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 51; - pos_bol = 2194; - pos_cnum = 2208 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 51; - pos_bol = 2194; - pos_cnum = 2241 - } - }))) - | (Length, Res ((Int, _), l_1)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l_1) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__008_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 58; - pos_bol = 2649; - pos_cnum = 2663 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 58; - pos_bol = 2649; - pos_cnum = 2693 - } - }))) - | (Add_l a_1, Res ((Node (Int), _), n)) -> true - | (Add_r a_2, Res ((Node (Int), _), n_1)) -> true - | (Take_l, Res ((Result (Int, Exn), _), a_3)) -> - (match a_3 with - | Ok a_3 -> - (try - if - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - a_3 = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__006_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 85; - pos_bol = 4320; - pos_cnum = 4334 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 87; - pos_bol = 4394; - pos_cnum = 4445 - } - }))) - | Error (Empty) -> - (try - let __t1__009_ = - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - let __t2__010_ = - Ortac_runtime.Gospelstdlib.Sequence.empty = - (Lazy.force new_state__008_).contents in - __t1__009_ && __t2__010_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 88; - pos_bol = 4446; - pos_cnum = 4468 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 88; - pos_bol = 4446; - pos_cnum = 4512 - } - }))) - | _ -> false) - | (Take_r, Res ((Result (Int, Exn), _), a_4)) -> - (match a_4 with - | Ok a_4 -> - (try - if - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - a_4 = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__006_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__006_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 99; - pos_bol = 5153; - pos_cnum = 5167 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 101; - pos_bol = 5227; - pos_cnum = 5304 - } - }))) - | Error (Empty) -> - (try - let __t1__011_ = - state__006_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - let __t2__012_ = - Ortac_runtime.Gospelstdlib.Sequence.empty = - (Lazy.force new_state__008_).contents in - __t1__011_ && __t2__012_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 102; - pos_bol = 5305; - pos_cnum = 5327 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 102; - pos_bol = 5305; - pos_cnum = 5371 - } - }))) - | _ -> false) - | (Take_opt_l, Res ((Option (Int), _), o)) -> - (try - state__006_.contents = - (match o with - | None -> Ortac_runtime.Gospelstdlib.Sequence.empty - | Some a_5 -> - Ortac_runtime.Gospelstdlib.Sequence.cons a_5 - (Lazy.force new_state__008_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 112; - pos_bol = 6030; - pos_cnum = 6044 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 114; - pos_bol = 6131; - pos_cnum = 6201 - } - }))) - | (Take_opt_r, Res ((Option (Int), _), o_1)) -> - (try - state__006_.contents = - (match o_1 with - | None -> Ortac_runtime.Gospelstdlib.Sequence.empty - | Some a_6 -> - Ortac_runtime.Gospelstdlib.Sequence.snoc - (Lazy.force new_state__008_).contents a_6) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 124; - pos_bol = 6869; - pos_cnum = 6883 - }; - Ortac_runtime.stop = - { - pos_fname = "lwt_dllist_spec.mli"; - pos_lnum = 126; - pos_bol = 6970; - pos_cnum = 7040 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__015_ sut__016_ = match cmd__015_ with | Is_empty -> Res (bool, (is_empty sut__016_)) @@ -543,12 +297,424 @@ module Spec = | Take_opt_l -> Res ((option int), (take_opt_l sut__016_)) | Take_opt_r -> Res ((option int), (take_opt_r sut__016_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__005_ state__006_ res__007_ = + let open Spec in + let open STM in + let new_state__008_ = lazy (next_state cmd__005_ state__006_) in + match (cmd__005_, res__007_) with + | (Is_empty, Res ((Bool, _), b)) -> + if + (try + (b = true) = + ((Lazy.force new_state__008_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2208 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2241 + } + }))) + then [] + else + [("is_empty", "b <-> s.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2208 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 51; + pos_bol = 2194; + pos_cnum = 2241 + } + })] + | (Length, Res ((Int, _), l_1)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int l_1) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__008_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2663 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2693 + } + }))) + then [] + else + [("length", "l = Sequence.length s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2663 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 58; + pos_bol = 2649; + pos_cnum = 2693 + } + })] + | (Add_l a_1, Res ((Node (Int), _), n)) -> [] + | (Add_r a_2, Res ((Node (Int), _), n_1)) -> [] + | (Take_l, Res ((Result (Int, Exn), _), a_3)) -> + (match a_3 with + | Ok a_3 -> + if + (try + if + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + a_3 = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__006_.contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 85; + pos_bol = 4320; + pos_cnum = 4334 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 87; + pos_bol = 4394; + pos_cnum = 4445 + } + }))) + then [] + else + [("take_l", + "if old s.contents = Sequence.empty\n then false\n else a = Sequence.hd (old s.contents)", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 85; + pos_bol = 4320; + pos_cnum = 4334 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 87; + pos_bol = 4394; + pos_cnum = 4445 + } + })] + | Error (Empty) -> + if + (try + let __t1__009_ = + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + let __t2__010_ = + Ortac_runtime.Gospelstdlib.Sequence.empty = + (Lazy.force new_state__008_).contents in + __t1__009_ && __t2__010_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4468 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4512 + } + }))) + then [] + else + [("take_l", "old s.contents = Sequence.empty = s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4468 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 88; + pos_bol = 4446; + pos_cnum = 4512 + } + })] + | _ -> []) + | (Take_r, Res ((Result (Int, Exn), _), a_4)) -> + (match a_4 with + | Ok a_4 -> + if + (try + if + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + a_4 = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__006_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__006_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 99; + pos_bol = 5153; + pos_cnum = 5167 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 101; + pos_bol = 5227; + pos_cnum = 5304 + } + }))) + then [] + else + [("take_r", + "if old s.contents = Sequence.empty\n then false\n else a = (old s.contents)[Sequence.length (old s.contents) - 1]", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 99; + pos_bol = 5153; + pos_cnum = 5167 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 101; + pos_bol = 5227; + pos_cnum = 5304 + } + })] + | Error (Empty) -> + if + (try + let __t1__011_ = + state__006_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + let __t2__012_ = + Ortac_runtime.Gospelstdlib.Sequence.empty = + (Lazy.force new_state__008_).contents in + __t1__011_ && __t2__012_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5327 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5371 + } + }))) + then [] + else + [("take_r", "old s.contents = Sequence.empty = s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5327 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 102; + pos_bol = 5305; + pos_cnum = 5371 + } + })] + | _ -> []) + | (Take_opt_l, Res ((Option (Int), _), o)) -> + if + (try + state__006_.contents = + (match o with + | None -> Ortac_runtime.Gospelstdlib.Sequence.empty + | Some a_5 -> + Ortac_runtime.Gospelstdlib.Sequence.cons a_5 + (Lazy.force new_state__008_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 112; + pos_bol = 6030; + pos_cnum = 6044 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 114; + pos_bol = 6131; + pos_cnum = 6201 + } + }))) + then [] + else + [("take_opt_l", + "old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.cons a s.contents", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 112; + pos_bol = 6030; + pos_cnum = 6044 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 114; + pos_bol = 6131; + pos_cnum = 6201 + } + })] + | (Take_opt_r, Res ((Option (Int), _), o_1)) -> + if + (try + state__006_.contents = + (match o_1 with + | None -> Ortac_runtime.Gospelstdlib.Sequence.empty + | Some a_6 -> + Ortac_runtime.Gospelstdlib.Sequence.snoc + (Lazy.force new_state__008_).contents a_6) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 124; + pos_bol = 6869; + pos_cnum = 6883 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 126; + pos_bol = 6970; + pos_cnum = 7040 + } + }))) + then [] + else + [("take_opt_r", + "old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.snoc s.contents a", + { + Ortac_runtime.start = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 124; + pos_bol = 6869; + pos_cnum = 6883 + }; + Ortac_runtime.stop = + { + pos_fname = "lwt_dllist_spec.mli"; + pos_lnum = 126; + pos_bol = 6970; + pos_cnum = 7040 + } + })] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Lwt_dllist_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Lwt_dllist_spec STM tests" + wrapped_init_state ortac_postcond]) diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index fcc9ba4c..204b7098 100644 --- a/examples/varray_circular_tests.ml +++ b/examples/varray_circular_tests.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Varray_circular_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm let inside i s = try if @@ -58,7 +60,6 @@ let proj e = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Varray_incl type sut = char t type cmd = @@ -666,215 +667,121 @@ module Spec = | Length -> true | Is_empty -> true | Fill (pos, len, x_3) -> true - let postcond cmd__016_ state__017_ res__018_ = + let postcond _ _ _ = true + let run cmd__032_ sut__033_ = + match cmd__032_ with + | Push_back x -> Res (unit, (push_back sut__033_ x)) + | Pop_back -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_back sut__033_) ())) + | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) + | Pop_front -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_front sut__033_) ())) + | Insert_at (i_1, x_2) -> + Res + ((result unit exn), + (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) + | Pop_at i_2 -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_at sut__033_ i_2) ())) + | Delete_at i_3 -> + Res + ((result unit exn), + (protect (fun () -> delete_at sut__033_ i_3) ())) + | Get i_4 -> + Res + ((result (elt char) exn), + (protect (fun () -> get sut__033_ i_4) ())) + | Set (i_5, v) -> + Res + ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) + | Length -> Res (int, (length sut__033_)) + | Is_empty -> Res (bool, (is_empty sut__033_)) + | Fill (pos, len, x_3) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__033_ pos len x_3) ())) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let wrapped_init_state () = Spec.init_state +let ortac_postcond cmd__016_ state__017_ res__018_ = + let open Spec in + let open STM in let new_state__019_ = lazy (next_state cmd__016_ state__017_) in match (cmd__016_, res__018_) with - | (Push_back x, Res ((Unit, _), _)) -> true + | (Push_back x, Res ((Unit, _), _)) -> [] | (Pop_back, Res ((Result (Elt (Char), Exn), _), x_4)) -> (match x_4 with | Ok x_4 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_4) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 33; - pos_bol = 2340; - pos_cnum = 2354 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 35; - pos_bol = 2414; - pos_cnum = 2496 - } - }))) - | Error (Not_found) -> - (try - let __t1__020_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__021_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__020_ && __t2__021_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 36; - pos_bol = 2497; - pos_cnum = 2523 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 36; - pos_bol = 2497; - pos_cnum = 2567 - } - }))) - | _ -> false) - | (Push_front x_1, Res ((Unit, _), _)) -> true - | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> - (match x_5 with - | Ok x_5 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_5) = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__017_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 56; - pos_bol = 3884; - pos_cnum = 3898 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 58; - pos_bol = 3958; - pos_cnum = 4014 - } - }))) - | Error (Not_found) -> - (try - let __t1__022_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__023_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__022_ && __t2__023_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 59; - pos_bol = 4015; - pos_cnum = 4041 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 59; - pos_bol = 4015; - pos_cnum = 4085 - } - }))) - | _ -> false) - | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__024_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__025_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__024_ && __t2__025_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + if + (try + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_4) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 33; + pos_bol = 2340; + pos_cnum = 2354 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 35; + pos_bol = 2414; + pos_cnum = 2496 + } + }))) + then [] + else + [("pop_back", + "if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 72; - pos_bol = 4784; - pos_cnum = 4797 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 72; - pos_bol = 4784; - pos_cnum = 4833 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 33; + pos_bol = 2340; + pos_cnum = 2354 + }; + Ortac_runtime.stop = { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 89; - pos_bol = 5727; - pos_cnum = 5740 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 89; - pos_bol = 5727; - pos_cnum = 5759 - } - }))) - then - (match x_6 with - | Ok x_6 -> + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 35; + pos_bol = 2414; + pos_cnum = 2496 + } + })] + | Error (Not_found) -> + if (try - (proj x_6) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + let __t1__020_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__021_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__020_ && __t2__021_ with | e -> raise @@ -884,59 +791,53 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 92; - pos_bol = 5864; - pos_cnum = 5878 + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2523 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 92; - pos_bol = 5864; - pos_cnum = 5906 + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2567 } }))) - | _ -> false) - else - (match x_6 with | Error (Invalid_argument _) -> true | _ -> false) - | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_back", + "t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 102; - pos_bol = 6426; - pos_cnum = 6439 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 102; - pos_bol = 6426; - pos_cnum = 6458 - } - }))) - then - (match res with - | Ok _ -> + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2523 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 36; + pos_bol = 2497; + pos_cnum = 2567 + } + })] + | _ -> []) + | (Push_front x_1, Res ((Unit, _), _)) -> [] + | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> + (match x_5 with + | Ok x_5 -> + if (try - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - = - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_5) = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__017_.contents) with | e -> raise @@ -946,56 +847,48 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 105; - pos_bol = 6563; - pos_cnum = 6577 + pos_lnum = 56; + pos_bol = 3884; + pos_cnum = 3898 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 105; - pos_bol = 6563; - pos_cnum = 6642 + pos_lnum = 58; + pos_bol = 3958; + pos_cnum = 4014 } }))) - | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_front", + "if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 128; - pos_bol = 7616; - pos_cnum = 7629 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 128; - pos_bol = 7616; - pos_cnum = 7648 - } - }))) - then - (match x_7 with - | Ok x_7 -> + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 56; + pos_bol = 3884; + pos_cnum = 3898 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 58; + pos_bol = 3958; + pos_cnum = 4014 + } + })] + | Error (Not_found) -> + if (try - (proj x_7) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - (Lazy.force new_state__019_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + let __t1__022_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__023_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__022_ && __t2__023_ with | e -> raise @@ -1005,124 +898,715 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 127; - pos_bol = 7577; - pos_cnum = 7591 + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4041 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 127; - pos_bol = 7577; - pos_cnum = 7615 + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4085 } }))) - | _ -> false) - else - (match x_7 with | Error (Invalid_argument _) -> true | _ -> false) - | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_front", + "t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 137; - pos_bol = 8077; - pos_cnum = 8090 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_circular_spec.mli"; - pos_lnum = 137; - pos_bol = 8077; - pos_cnum = 8109 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Length, Res ((Int, _), l)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4041 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 59; + pos_bol = 4015; + pos_cnum = 4085 + } + })] + | _ -> []) + | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })) + then [] + else + [("insert_at", "0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })] with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + }))) + then [] + else + [("insert_at", "0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4797 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 72; + pos_bol = 4784; + pos_cnum = 4833 + } + })])) + | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + })) + then [] + else + [("pop_at", "inside i t.contents", { Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 144; - pos_bol = 8634; - pos_cnum = 8648 + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 144; - pos_bol = 8634; - pos_cnum = 8678 + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 } - }))) - | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__019_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) + })] with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + | [] -> + (match x_6 with + | Ok x_6 -> + if + (try + (proj x_6) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5878 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5906 + } + }))) + then [] + else + [("pop_at", "(proj x) = old t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5878 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 92; + pos_bol = 5864; + pos_cnum = 5906 + } + })] + | _ -> []) + | _ -> + (match x_6 with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + }))) + then [] + else + [("pop_at", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5740 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 89; + pos_bol = 5727; + pos_cnum = 5759 + } + })])) + | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + })) + then [] + else + [("delete_at", "inside i t.contents", { Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 171; - pos_bol = 10238; - pos_cnum = 10252 + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 171; - pos_bol = 10238; - pos_cnum = 10285 + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 } - }))) - | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + })] + with + | [] -> + (match res with + | Ok _ -> + if + (try + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) + = + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6577 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6642 + } + }))) + then [] + else + [("delete_at", + "Sequence.length t.contents = Sequence.length (old t.contents) - 1", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6577 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 105; + pos_bol = 6563; + pos_cnum = 6642 + } + })] + | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + }))) + then [] + else + [("delete_at", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6439 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 102; + pos_bol = 6426; + pos_cnum = 6458 + } + })])) + | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })) + then [] + else + [("get", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })] + with + | [] -> + (match x_7 with + | Ok x_7 -> + if + (try + (proj x_7) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + (Lazy.force new_state__019_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7591 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7615 + } + }))) + then [] + else + [("get", "(proj x) = t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7591 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 127; + pos_bol = 7577; + pos_cnum = 7615 + } + })] + | _ -> []) + | _ -> + (match x_7 with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + }))) + then [] + else + [("get", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7629 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 128; + pos_bol = 7616; + pos_cnum = 7648 + } + })])) + | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })) + then [] + else + [("set", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + }))) + then [] + else + [("set", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8090 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 137; + pos_bol = 8077; + pos_cnum = 8109 + } + })])) + | (Length, Res ((Int, _), l)) -> if (try - let __t1__026_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) in - let __t2__027_ = - let __t1__028_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int len) in - let __t2__029_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) - (Ortac_runtime.Gospelstdlib.integer_of_int len)) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__028_ && __t2__029_ in - __t1__026_ && __t2__027_ + (Ortac_runtime.Gospelstdlib.integer_of_int l) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) with | e -> raise @@ -1132,66 +1616,219 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 211; - pos_bol = 12981; - pos_cnum = 12994 + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8648 }; Ortac_runtime.stop = { pos_fname = "varray_circular_spec.mli"; - pos_lnum = 211; - pos_bol = 12981; - pos_cnum = 13056 + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8678 } }))) - then (match res with | Ok _ -> true | _ -> false) + then [] else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true - let run cmd__032_ sut__033_ = - match cmd__032_ with - | Push_back x -> Res (unit, (push_back sut__033_ x)) - | Pop_back -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_back sut__033_) ())) - | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) - | Pop_front -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_front sut__033_) ())) - | Insert_at (i_1, x_2) -> - Res - ((result unit exn), - (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) - | Pop_at i_2 -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_at sut__033_ i_2) ())) - | Delete_at i_3 -> - Res - ((result unit exn), - (protect (fun () -> delete_at sut__033_ i_3) ())) - | Get i_4 -> - Res - ((result (elt char) exn), - (protect (fun () -> get sut__033_ i_4) ())) - | Set (i_5, v) -> - Res - ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) - | Length -> Res (int, (length sut__033_)) - | Is_empty -> Res (bool, (is_empty sut__033_)) - | Fill (pos, len, x_3) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__033_ pos len x_3) ())) - end -module STMTests = (STM_sequential.Make)(Spec) -let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs + [("length", "l = Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8648 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 144; + pos_bol = 8634; + pos_cnum = 8678 + } + })] + | (Is_empty, Res ((Bool, _), b)) -> + if + (try + (b = true) = + ((Lazy.force new_state__019_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10252 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10285 + } + }))) + then [] + else + [("is_empty", "b <-> t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10252 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 171; + pos_bol = 10238; + pos_cnum = 10285 + } + })] + | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) + (Ortac_runtime.Gospelstdlib.integer_of_int len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })) + then [] + else + [("fill", + "0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + pos) + (Ortac_runtime.Gospelstdlib.integer_of_int + len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = + "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + }))) + then [] + else + [("fill", + "0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 12994 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_circular_spec.mli"; + pos_lnum = 211; + pos_bol = 12981; + pos_cnum = 13056 + } + })])) + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Varray_circular_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Varray_circular_spec STM tests" + wrapped_init_state ortac_postcond]) diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml index 68f691b6..dd476130 100644 --- a/examples/varray_tests.ml +++ b/examples/varray_tests.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Varray_spec +module Ortac_runtime = Ortac_runtime_qcheck_stm let inside i s = try if @@ -58,7 +60,6 @@ let proj e = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] include Varray_incl type sut = char t type cmd = @@ -666,215 +667,121 @@ module Spec = | Length -> true | Is_empty -> true | Fill (pos, len, x_3) -> true - let postcond cmd__016_ state__017_ res__018_ = + let postcond _ _ _ = true + let run cmd__032_ sut__033_ = + match cmd__032_ with + | Push_back x -> Res (unit, (push_back sut__033_ x)) + | Pop_back -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_back sut__033_) ())) + | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) + | Pop_front -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_front sut__033_) ())) + | Insert_at (i_1, x_2) -> + Res + ((result unit exn), + (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) + | Pop_at i_2 -> + Res + ((result (elt char) exn), + (protect (fun () -> pop_at sut__033_ i_2) ())) + | Delete_at i_3 -> + Res + ((result unit exn), + (protect (fun () -> delete_at sut__033_ i_3) ())) + | Get i_4 -> + Res + ((result (elt char) exn), + (protect (fun () -> get sut__033_ i_4) ())) + | Set (i_5, v) -> + Res + ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) + | Length -> Res (int, (length sut__033_)) + | Is_empty -> Res (bool, (is_empty sut__033_)) + | Fill (pos, len, x_3) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__033_ pos len x_3) ())) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let wrapped_init_state () = Spec.init_state +let ortac_postcond cmd__016_ state__017_ res__018_ = + let open Spec in + let open STM in let new_state__019_ = lazy (next_state cmd__016_ state__017_) in match (cmd__016_, res__018_) with - | (Push_back x, Res ((Unit, _), _)) -> true + | (Push_back x, Res ((Unit, _), _)) -> [] | (Pop_back, Res ((Result (Elt (Char), Exn), _), x_4)) -> (match x_4 with | Ok x_4 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_4) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1))) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 33; - pos_bol = 2160; - pos_cnum = 2174 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 35; - pos_bol = 2234; - pos_cnum = 2316 - } - }))) - | Error (Not_found) -> - (try - let __t1__020_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__021_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__020_ && __t2__021_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 36; - pos_bol = 2317; - pos_cnum = 2343 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 36; - pos_bol = 2317; - pos_cnum = 2387 - } - }))) - | _ -> false) - | (Push_front x_1, Res ((Unit, _), _)) -> true - | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> - (match x_5 with - | Ok x_5 -> - (try - if - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty - then false - else - (proj x_5) = - (Ortac_runtime.Gospelstdlib.Sequence.hd - state__017_.contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 56; - pos_bol = 3632; - pos_cnum = 3646 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 58; - pos_bol = 3706; - pos_cnum = 3762 - } - }))) - | Error (Not_found) -> - (try - let __t1__022_ = - (Lazy.force new_state__019_).contents = - state__017_.contents in - let __t2__023_ = - state__017_.contents = - Ortac_runtime.Gospelstdlib.Sequence.empty in - __t1__022_ && __t2__023_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 59; - pos_bol = 3763; - pos_cnum = 3789 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 59; - pos_bol = 3763; - pos_cnum = 3833 - } - }))) - | _ -> false) - | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__024_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__025_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__024_ && __t2__025_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + if + (try + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_4) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1))) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 33; + pos_bol = 2160; + pos_cnum = 2174 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 35; + pos_bol = 2234; + pos_cnum = 2316 + } + }))) + then [] + else + [("pop_back", + "if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 72; - pos_bol = 4496; - pos_cnum = 4509 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 72; - pos_bol = 4496; - pos_cnum = 4545 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + pos_fname = "varray_spec.mli"; + pos_lnum = 33; + pos_bol = 2160; + pos_cnum = 2174 + }; + Ortac_runtime.stop = { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 89; - pos_bol = 5403; - pos_cnum = 5416 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 89; - pos_bol = 5403; - pos_cnum = 5435 - } - }))) - then - (match x_6 with - | Ok x_6 -> + pos_fname = "varray_spec.mli"; + pos_lnum = 35; + pos_bol = 2234; + pos_cnum = 2316 + } + })] + | Error (Not_found) -> + if (try - (proj x_6) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - state__017_.contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + let __t1__020_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__021_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__020_ && __t2__021_ with | e -> raise @@ -884,59 +791,53 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 92; - pos_bol = 5540; - pos_cnum = 5554 + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2343 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 92; - pos_bol = 5540; - pos_cnum = 5582 + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2387 } }))) - | _ -> false) - else - (match x_6 with | Error (Invalid_argument _) -> true | _ -> false) - | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_back", + "t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 102; - pos_bol = 6066; - pos_cnum = 6079 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 102; - pos_bol = 6066; - pos_cnum = 6098 - } - }))) - then - (match res with - | Ok _ -> + pos_fname = "varray_spec.mli"; + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2343 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 36; + pos_bol = 2317; + pos_cnum = 2387 + } + })] + | _ -> []) + | (Push_front x_1, Res ((Unit, _), _)) -> [] + | (Pop_front, Res ((Result (Elt (Char), Exn), _), x_5)) -> + (match x_5 with + | Ok x_5 -> + if (try - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) - = - (Ortac_runtime.Gospelstdlib.(-) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + if + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty + then false + else + (proj x_5) = + (Ortac_runtime.Gospelstdlib.Sequence.hd + state__017_.contents) with | e -> raise @@ -946,56 +847,48 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 105; - pos_bol = 6203; - pos_cnum = 6217 + pos_lnum = 56; + pos_bol = 3632; + pos_cnum = 3646 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 105; - pos_bol = 6203; - pos_cnum = 6282 + pos_lnum = 58; + pos_bol = 3706; + pos_cnum = 3762 } }))) - | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_front", + "if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 128; - pos_bol = 7220; - pos_cnum = 7233 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 128; - pos_bol = 7220; - pos_cnum = 7252 - } - }))) - then - (match x_7 with - | Ok x_7 -> + pos_fname = "varray_spec.mli"; + pos_lnum = 56; + pos_bol = 3632; + pos_cnum = 3646 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 58; + pos_bol = 3706; + pos_cnum = 3762 + } + })] + | Error (Not_found) -> + if (try - (proj x_7) = - (Ortac_runtime.Gospelstdlib.__mix_Bub - (Lazy.force new_state__019_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + let __t1__022_ = + (Lazy.force new_state__019_).contents = + state__017_.contents in + let __t2__023_ = + state__017_.contents = + Ortac_runtime.Gospelstdlib.Sequence.empty in + __t1__022_ && __t2__023_ with | e -> raise @@ -1005,124 +898,699 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 127; - pos_bol = 7181; - pos_cnum = 7195 + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3789 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 127; - pos_bol = 7181; - pos_cnum = 7219 + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3833 } }))) - | _ -> false) - else - (match x_7 with | Error (Invalid_argument _) -> true | _ -> false) - | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> - if - (try - (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) - state__017_.contents) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("pop_front", + "t.contents = old t.contents = Sequence.empty", + { + Ortac_runtime.start = { - Ortac_runtime.start = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 137; - pos_bol = 7645; - pos_cnum = 7658 - }; - Ortac_runtime.stop = - { - pos_fname = "varray_spec.mli"; - pos_lnum = 137; - pos_bol = 7645; - pos_cnum = 7677 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Length, Res ((Int, _), l)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int l) = - (Ortac_runtime.Gospelstdlib.Sequence.length - (Lazy.force new_state__019_).contents) + pos_fname = "varray_spec.mli"; + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3789 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 59; + pos_bol = 3763; + pos_cnum = 3833 + } + })] + | _ -> []) + | (Insert_at (i_1, x_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })) + then [] + else + [("insert_at", "0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })] with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__024_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__025_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__024_ && __t2__025_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + }))) + then [] + else + [("insert_at", "0 <= i <= Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4509 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 72; + pos_bol = 4496; + pos_cnum = 4545 + } + })])) + | (Pop_at i_2, Res ((Result (Elt (Char), Exn), _), x_6)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + })) + then [] + else + [("pop_at", "inside i t.contents", { Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 144; - pos_bol = 8166; - pos_cnum = 8180 + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 144; - pos_bol = 8166; - pos_cnum = 8210 + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 } - }))) - | (Is_empty, Res ((Bool, _), b)) -> - (try - (b = true) = - ((Lazy.force new_state__019_).contents = - Ortac_runtime.Gospelstdlib.Sequence.empty) + })] with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + | [] -> + (match x_6 with + | Ok x_6 -> + if + (try + (proj x_6) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + state__017_.contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5554 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5582 + } + }))) + then [] + else + [("pop_at", "(proj x) = old t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5554 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 92; + pos_bol = 5540; + pos_cnum = 5582 + } + })] + | _ -> []) + | _ -> + (match x_6 with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + }))) + then [] + else + [("pop_at", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5416 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 89; + pos_bol = 5403; + pos_cnum = 5435 + } + })])) + | (Delete_at i_3, Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + })) + then [] + else + [("delete_at", "inside i t.contents", { Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 171; - pos_bol = 9662; - pos_cnum = 9676 + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 171; - pos_bol = 9662; - pos_cnum = 9709 + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 } - }))) - | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + })] + with + | [] -> + (match res with + | Ok _ -> + if + (try + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) + = + (Ortac_runtime.Gospelstdlib.(-) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6217 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6282 + } + }))) + then [] + else + [("delete_at", + "Sequence.length t.contents = Sequence.length (old t.contents) - 1", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6217 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 105; + pos_bol = 6203; + pos_cnum = 6282 + } + })] + | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_3) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + }))) + then [] + else + [("delete_at", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6079 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 102; + pos_bol = 6066; + pos_cnum = 6098 + } + })])) + | (Get i_4, Res ((Result (Elt (Char), Exn), _), x_7)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })) + then [] + else + [("get", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })] + with + | [] -> + (match x_7 with + | Ok x_7 -> + if + (try + (proj x_7) = + (Ortac_runtime.Gospelstdlib.__mix_Bub + (Lazy.force new_state__019_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i_4)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7195 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7219 + } + }))) + then [] + else + [("get", "(proj x) = t.contents[i]", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7195 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 127; + pos_bol = 7181; + pos_cnum = 7219 + } + })] + | _ -> []) + | _ -> + (match x_7 with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_4) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + }))) + then [] + else + [("get", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7233 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 128; + pos_bol = 7220; + pos_cnum = 7252 + } + })])) + | (Set (i_5, v), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + (inside (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })) + then [] + else + [("set", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + (inside + (Ortac_runtime.Gospelstdlib.integer_of_int i_5) + state__017_.contents) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + }))) + then [] + else + [("set", "inside i t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7658 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 137; + pos_bol = 7645; + pos_cnum = 7677 + } + })])) + | (Length, Res ((Int, _), l)) -> if (try - let __t1__026_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) in - let __t2__027_ = - let __t1__028_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int len) in - let __t2__029_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int pos) - (Ortac_runtime.Gospelstdlib.integer_of_int len)) - (Ortac_runtime.Gospelstdlib.Sequence.length - state__017_.contents) in - __t1__028_ && __t2__029_ in - __t1__026_ && __t2__027_ + (Ortac_runtime.Gospelstdlib.integer_of_int l) = + (Ortac_runtime.Gospelstdlib.Sequence.length + (Lazy.force new_state__019_).contents) with | e -> raise @@ -1132,66 +1600,217 @@ module Spec = Ortac_runtime.start = { pos_fname = "varray_spec.mli"; - pos_lnum = 211; - pos_bol = 12225; - pos_cnum = 12238 + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8180 }; Ortac_runtime.stop = { pos_fname = "varray_spec.mli"; - pos_lnum = 211; - pos_bol = 12225; - pos_cnum = 12300 + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8210 } }))) - then (match res with | Ok _ -> true | _ -> false) + then [] else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true - let run cmd__032_ sut__033_ = - match cmd__032_ with - | Push_back x -> Res (unit, (push_back sut__033_ x)) - | Pop_back -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_back sut__033_) ())) - | Push_front x_1 -> Res (unit, (push_front sut__033_ x_1)) - | Pop_front -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_front sut__033_) ())) - | Insert_at (i_1, x_2) -> - Res - ((result unit exn), - (protect (fun () -> insert_at sut__033_ i_1 x_2) ())) - | Pop_at i_2 -> - Res - ((result (elt char) exn), - (protect (fun () -> pop_at sut__033_ i_2) ())) - | Delete_at i_3 -> - Res - ((result unit exn), - (protect (fun () -> delete_at sut__033_ i_3) ())) - | Get i_4 -> - Res - ((result (elt char) exn), - (protect (fun () -> get sut__033_ i_4) ())) - | Set (i_5, v) -> - Res - ((result unit exn), (protect (fun () -> set sut__033_ i_5 v) ())) - | Length -> Res (int, (length sut__033_)) - | Is_empty -> Res (bool, (is_empty sut__033_)) - | Fill (pos, len, x_3) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__033_ pos len x_3) ())) - end -module STMTests = (STM_sequential.Make)(Spec) -let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs + [("length", "l = Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8180 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 144; + pos_bol = 8166; + pos_cnum = 8210 + } + })] + | (Is_empty, Res ((Bool, _), b)) -> + if + (try + (b = true) = + ((Lazy.force new_state__019_).contents = + Ortac_runtime.Gospelstdlib.Sequence.empty) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9676 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9709 + } + }))) + then [] + else + [("is_empty", "b <-> t.contents = Sequence.empty", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9676 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 171; + pos_bol = 9662; + pos_cnum = 9709 + } + })] + | (Fill (pos, len, x_3), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) + (Ortac_runtime.Gospelstdlib.integer_of_int len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })) + then [] + else + [("fill", + "0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__026_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int pos) in + let __t2__027_ = + let __t1__028_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int len) in + let __t2__029_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + pos) + (Ortac_runtime.Gospelstdlib.integer_of_int + len)) + (Ortac_runtime.Gospelstdlib.Sequence.length + state__017_.contents) in + __t1__028_ && __t2__029_ in + __t1__026_ && __t2__027_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + }))) + then [] + else + [("fill", + "0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12238 + }; + Ortac_runtime.stop = + { + pos_fname = "varray_spec.mli"; + pos_lnum = 211; + pos_bol = 12225; + pos_cnum = 12300 + } + })])) + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Varray_spec STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Varray_spec STM tests" + wrapped_init_state ortac_postcond]) diff --git a/ortac-runtime-qcheck-stm.opam b/ortac-runtime-qcheck-stm.opam new file mode 100644 index 00000000..ff6e938c --- /dev/null +++ b/ortac-runtime-qcheck-stm.opam @@ -0,0 +1,40 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Runtime support library for Ortac/QCheck-STM-generated code" +description: """ +The ortac-runtime-qcheck-stm library provides support for the code +generated by the Ortac/QCheck-STM plugin (provided by the +ortac-qcheck-stm package). + +Ortac (OCaml Runtime Assertion Checking) is a tool to turn +executable Gospel specifications into code to test they hold. +""" +maintainer: ["Nicolas Osborne "] +authors: ["Nicolas Osborne "] +license: "MIT" +homepage: "https://github.com/ocaml-gospel/ortac" +bug-reports: "https://github.com/ocaml-gospel/ortac/issues" +depends: [ + "dune" {>= "3.8"} + "ocaml" {>= "4.11.0"} + "qcheck-stm" + "ortac-runtime" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/ocaml-gospel/ortac.git" diff --git a/plugins/qcheck-stm/src/runtime/dune b/plugins/qcheck-stm/src/runtime/dune new file mode 100644 index 00000000..5f367d15 --- /dev/null +++ b/plugins/qcheck-stm/src/runtime/dune @@ -0,0 +1,10 @@ +(library + (name ortac_runtime_qcheck_stm) + (public_name ortac-runtime-qcheck-stm) + (libraries + qcheck-core + qcheck-core.runner + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime)) diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml new file mode 100644 index 00000000..70f60095 --- /dev/null +++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml @@ -0,0 +1,75 @@ +open STM +include Ortac_runtime + +type stm_disagree = { term : string } + +module Make (Spec : Spec) = struct + open QCheck + module Internal = Internal.Make (Spec) [@alert "-internal"] + + let print_seq_trace trace = + List.fold_left + (fun acc (c, r) -> + Printf.sprintf "%s\n %s : %s" acc (Spec.show_cmd c) (show_res r)) + "" trace + + let pp_trace trace = + let open Fmt in + let pp_aux ppf (c, r) = + pf ppf "%s : %s@\n" (Spec.show_cmd c) (show_res r) + in + str "%a" (list pp_aux) trace + + let pp_err err = + let open Fmt in + let pp_aux ppf (cmd, term, l) = + pf ppf "%s violated the specification in %a:@\n@\n @[%a@]@." cmd pp_loc l + (list string) term + in + str "%a" (list pp_aux) err + + let pp_trace_and_err trace err = + let open Fmt in + str + "Gospel specification violation@\n\ + \ @[%s@]@\n\ + when executing this sequence of operations:@\n\ + @[%s@]@." + (pp_err err) (pp_trace trace) + + let rec check_disagree postcond s sut cs = + match cs with + | [] -> None + | c :: cs -> ( + let res = Spec.run c sut in + (* This functor will be called after a modified postcond has been defined, + returning a list of 3-plets of strings representing the command, the + term and the location *) + match postcond c s res with + | [] -> ( + let s' = Spec.next_state c s in + match check_disagree postcond s' sut cs with + | None -> None + | Some (rest, err) -> Some ((c, res) :: rest, err)) + | err -> Some ([ (c, res) ], err)) + + let agree_prop wrapped_init_state postcond cs = + let _ = wrapped_init_state () in + assume (Internal.cmds_ok Spec.init_state cs); + let sut = Spec.init_sut () in + (* reset system's state *) + let res = + try Ok (check_disagree postcond Spec.init_state sut cs) + with exn -> Error exn + in + let () = Spec.cleanup sut in + let res = match res with Ok res -> res | Error exn -> raise exn in + match res with + | None -> true + | Some (trace, err) -> Test.fail_report @@ pp_trace_and_err trace err + + let agree_test ~count ~name wrapped_init_state postcond = + Test.make ~name ~count + (Internal.arb_cmds Spec.init_state) + (agree_prop wrapped_init_state postcond) +end diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 32541725..9407d9d7 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -445,9 +445,7 @@ let postcond_case config state invariants idx state_ident new_state_ident value and wrap_check t e = let term = estring t.text and cmd = Fmt.str "%a" Ident.pp value.id |> estring - and l = - Fmt.str "%a" Location.print t.Ir.term.Gospel.Tterm.t_loc |> estring - in + and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation in pexp_ifthenelse e (pexp_construct (lident "[]") None) (Some [%expr [ ([%e cmd], [%e term], [%e l]) ]]) @@ -919,7 +917,7 @@ let stm include_ config ir = (module_binding ~name:(noloc (Some "STMTests")) ~expr: (pmod_apply - (pmod_ident (Ldot (Lident "STM_sequential", "Make") |> noloc)) + (pmod_ident (Ldot (Lident "Ortac_runtime", "Make") |> noloc)) (pmod_ident (lident "Spec")))) in let module_name = Ortac_core.Context.module_name config.context in @@ -928,16 +926,16 @@ let stm include_ config ir = let descr = estring (module_name ^ " STM tests") in [%stri let _ = - let open QCheck in QCheck_base_runner.run_tests_main (let count = 1000 in [ - Test.make ~count ~name:[%e descr] - (STMTests.arb_cmds Spec.init_state) - agree_prop; + STMTests.agree_test ~count ~name:[%e descr] wrapped_init_state + ortac_postcond; ])] in ok - ((warn :: open_mod module_name :: ghost_functions) - @ [ stm_spec; tests; wrapped_init_state; postcond; agree_prop; call_tests ] - ) + (warn + :: open_mod module_name + :: [%stri module Ortac_runtime = Ortac_runtime_qcheck_stm] + :: ghost_functions + @ [ stm_spec; tests; wrapped_init_state; postcond; call_tests ]) diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml index c2532b68..3e475568 100644 --- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml @@ -1,8 +1,9 @@ +[@@@ocaml.warning "-26-27"] open Array +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Length @@ -309,45 +310,33 @@ module Spec = | Fill (i_2, j, a_2) -> true | To_list -> true | Mem a_3 -> true - let postcond cmd__008_ state__009_ res__010_ = + let postcond _ _ _ = true + let run cmd__018_ sut__019_ = + match cmd__018_ with + | Length -> Res (int, (length sut__019_)) + | Get i -> + Res ((result char exn), (protect (fun () -> get sut__019_ i) ())) + | Set (i_1, a_1) -> + Res + ((result unit exn), + (protect (fun () -> set sut__019_ i_1 a_1) ())) + | Fill (i_2, j, a_2) -> + Res + ((result unit exn), + (protect (fun () -> fill sut__019_ i_2 j a_2) ())) + | To_list -> Res ((list char), (to_list sut__019_)) + | Mem a_3 -> Res (bool, (mem a_3 sut__019_)) + end +module STMTests = (Ortac_runtime.Make)(Spec) +let wrapped_init_state () = Spec.init_state +let ortac_postcond cmd__008_ state__009_ res__010_ = + let open Spec in + let open STM in let new_state__011_ = lazy (next_state cmd__008_ state__009_) in match (cmd__008_, res__010_) with | (Length, Res ((Int, _), i_3)) -> - (try i_3 = (Lazy.force new_state__011_).size - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 7; - pos_bol = 238; - pos_cnum = 250 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 7; - pos_bol = 238; - pos_cnum = 260 - } - }))) - | (Get i, Res ((Result (Char, Exn), _), a_4)) -> if - (try - let __t1__012_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i) in - let __t2__013_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) in - __t1__012_ && __t2__013_ + (try i_3 = (Lazy.force new_state__011_).size with | e -> raise @@ -357,63 +346,601 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 11; - pos_bol = 378; - pos_cnum = 389 + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 250 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 11; - pos_bol = 378; - pos_cnum = 404 + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 260 } }))) - then - (match a_4 with - | Ok a_4 -> - (try - a_4 = - (Ortac_runtime.Gospelstdlib.List.nth - (Lazy.force new_state__011_).contents - (Ortac_runtime.Gospelstdlib.integer_of_int i)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, + then [] + else + [("length", "i = t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 250 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 7; + pos_bol = 238; + pos_cnum = 260 + } + })] + | (Get i, Res ((Result (Char, Exn), _), a_4)) -> + (match if + try + let __t1__012_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i) in + let __t2__013_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__012_ && __t2__013_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })) + then [] + else + [("get", "0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })] + with + | [] -> + (match a_4 with + | Ok a_4 -> + if + (try + a_4 = + (Ortac_runtime.Gospelstdlib.List.nth + (Lazy.force new_state__011_).contents + (Ortac_runtime.Gospelstdlib.integer_of_int i)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 417 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 442 + } + }))) + then [] + else + [("get", "a = List.nth t.contents i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 417 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 12; + pos_bol = 405; + pos_cnum = 442 + } + })] + | _ -> []) + | _ -> + (match a_4 with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__012_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i) in + let __t2__013_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__012_ && __t2__013_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + }))) + then [] + else + [("get", "0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 389 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 11; + pos_bol = 378; + pos_cnum = 404 + } + })])) + | (Set (i_1, a_1), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__014_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__015_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__014_ && __t2__015_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })) + then [] + else + [("set", "0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__014_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__015_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) in + __t1__014_ && __t2__015_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + }))) + then [] + else + [("set", "0 <= i < t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 593 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 16; + pos_bol = 582; + pos_cnum = 608 + } + })])) + | (Fill (i_2, j, a_2), Res ((Result (Unit, Exn), _), res)) -> + (match (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })) + then [] + else + [("fill", "0 <= i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })]) + @ + ((if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int j) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })) + then [] + else + [("fill", "0 <= j", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })]) + @ + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + i_2) + (Ortac_runtime.Gospelstdlib.integer_of_int j)) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })) + then [] + else + [("fill", "i + j <= t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })])) + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + (if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })) + then [] + else + [("fill", "0 <= i", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1194 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 28; + pos_bol = 1183; + pos_cnum = 1200 + } + })]) + @ + ((if + try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int j) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 + } + })) + then [] + else + [("fill", "0 <= j", { Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 12; - pos_bol = 405; - pos_cnum = 417 + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1212 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 12; - pos_bol = 405; - pos_cnum = 442 + pos_lnum = 29; + pos_bol = 1201; + pos_cnum = 1218 } - }))) - | _ -> false) - else - (match a_4 with | Error (Invalid_argument _) -> true | _ -> false) - | (Set (i_1, a_1), Res ((Result (Unit, Exn), _), res)) -> + })]) + @ + (if + (try + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int + i_2) + (Ortac_runtime.Gospelstdlib.integer_of_int + j)) + (Ortac_runtime.Gospelstdlib.integer_of_int + state__009_.size) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + }))) + then [] + else + [("fill", "i + j <= t.size", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1230 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 30; + pos_bol = 1219; + pos_cnum = 1245 + } + })])))) + | (To_list, Res ((List (Char), _), l)) -> if - (try - let __t1__014_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__015_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) in - __t1__014_ && __t2__015_ + (try l = (Lazy.force new_state__011_).contents with | e -> raise @@ -423,27 +950,43 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 16; - pos_bol = 582; - pos_cnum = 593 + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 16; - pos_bol = 582; - pos_cnum = 608 + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1585 } }))) - then (match res with | Ok _ -> true | _ -> false) + then [] else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (Fill (i_2, j, a_2), Res ((Result (Unit, Exn), _), res)) -> + [("to_list", "l = t.contents", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1585 + } + })] + | (Mem a_3, Res ((Bool, _), b)) -> if (try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) + (b = true) = + (Ortac_runtime.Gospelstdlib.List.mem a_3 + (Lazy.force new_state__011_).contents) with | e -> raise @@ -453,148 +996,40 @@ module Spec = Ortac_runtime.start = { pos_fname = "array.mli"; - pos_lnum = 28; - pos_bol = 1183; - pos_cnum = 1194 + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1721 }; Ortac_runtime.stop = { pos_fname = "array.mli"; - pos_lnum = 28; - pos_bol = 1183; - pos_cnum = 1200 + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1746 } }))) - && - ((try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int j) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 29; - pos_bol = 1201; - pos_cnum = 1212 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 29; - pos_bol = 1201; - pos_cnum = 1218 - } - }))) - && - ((try - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_2) - (Ortac_runtime.Gospelstdlib.integer_of_int j)) - (Ortac_runtime.Gospelstdlib.integer_of_int - state__009_.size) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 30; - pos_bol = 1219; - pos_cnum = 1230 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 30; - pos_bol = 1219; - pos_cnum = 1245 - } - }))))) - then (match res with | Ok _ -> true | _ -> false) + then [] else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | (To_list, Res ((List (Char), _), l)) -> - (try l = (Lazy.force new_state__011_).contents - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1585 - } - }))) - | (Mem a_3, Res ((Bool, _), b)) -> - (try - (b = true) = - (Ortac_runtime.Gospelstdlib.List.mem a_3 - (Lazy.force new_state__011_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "array.mli"; - pos_lnum = 40; - pos_bol = 1709; - pos_cnum = 1721 - }; - Ortac_runtime.stop = - { - pos_fname = "array.mli"; - pos_lnum = 40; - pos_bol = 1709; - pos_cnum = 1746 - } - }))) - | _ -> true - let run cmd__018_ sut__019_ = - match cmd__018_ with - | Length -> Res (int, (length sut__019_)) - | Get i -> - Res ((result char exn), (protect (fun () -> get sut__019_ i) ())) - | Set (i_1, a_1) -> - Res - ((result unit exn), - (protect (fun () -> set sut__019_ i_1 a_1) ())) - | Fill (i_2, j, a_2) -> - Res - ((result unit exn), - (protect (fun () -> fill sut__019_ i_2 j a_2) ())) - | To_list -> Res ((list char), (to_list sut__019_)) - | Mem a_3 -> Res (bool, (mem a_3 sut__019_)) - end -module STMTests = (STM_sequential.Make)(Spec) -let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs + [("mem", "b = List.mem a t.contents", + { + Ortac_runtime.start = + { + pos_fname = "array.mli"; + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1721 + }; + Ortac_runtime.stop = + { + pos_fname = "array.mli"; + pos_lnum = 40; + pos_bol = 1709; + pos_cnum = 1746 + } + })] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Array STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Array STM tests" wrapped_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml index e09e7b91..bb27f072 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Conjunctive_clauses +module Ortac_runtime = Ortac_runtime_qcheck_stm let set_contents c i a_1 = try Ortac_runtime.Gospelstdlib.List.mapi @@ -27,7 +29,6 @@ let set_contents c i a_1 = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Set of int * char @@ -144,47 +145,7 @@ module Spec = else state__003_ let precond cmd__012_ state__013_ = match cmd__012_ with | Set (i_1, a_2) -> true - let postcond cmd__006_ state__007_ res__008_ = - let new_state__009_ = lazy (next_state cmd__006_ state__007_) in - match (cmd__006_, res__008_) with - | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), res)) -> - if - (try - let __t1__010_ = - Ortac_runtime.Gospelstdlib.(<=) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in - let __t2__011_ = - Ortac_runtime.Gospelstdlib.(<) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.List.length - state__007_.contents) in - __t1__010_ && __t2__011_ - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 13; - pos_bol = 806; - pos_cnum = 817 - }; - Ortac_runtime.stop = - { - pos_fname = "conjunctive_clauses.mli"; - pos_lnum = 13; - pos_bol = 806; - pos_cnum = 848 - } - }))) - then (match res with | Ok _ -> true | _ -> false) - else - (match res with | Error (Invalid_argument _) -> true | _ -> false) - | _ -> true + let postcond _ _ _ = true let run cmd__014_ sut__015_ = match cmd__014_ with | Set (i_1, a_2) -> @@ -192,12 +153,127 @@ module Spec = ((result unit exn), (protect (fun () -> set sut__015_ i_1 a_2) ())) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__006_ state__007_ res__008_ = + let open Spec in + let open STM in + let new_state__009_ = lazy (next_state cmd__006_ state__007_) in + match (cmd__006_, res__008_) with + | (Set (i_1, a_2), Res ((Result (Unit, Exn), _), res)) -> + (match if + try + let __t1__010_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__011_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.List.length + state__007_.contents) in + __t1__010_ && __t2__011_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })) + then [] + else + [("set", "0 <= i < List.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })] + with + | [] -> (match res with | Ok _ -> [] | _ -> []) + | _ -> + (match res with + | Error (Invalid_argument _) -> [] + | _ -> + if + (try + let __t1__010_ = + Ortac_runtime.Gospelstdlib.(<=) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) in + let __t2__011_ = + Ortac_runtime.Gospelstdlib.(<) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.List.length + state__007_.contents) in + __t1__010_ && __t2__011_ + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + }))) + then [] + else + [("set", "0 <= i < List.length t.contents", + { + Ortac_runtime.start = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 817 + }; + Ortac_runtime.stop = + { + pos_fname = "conjunctive_clauses.mli"; + pos_lnum = 13; + pos_bol = 806; + pos_cnum = 848 + } + })])) + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Conjunctive_clauses STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Conjunctive_clauses STM tests" + wrapped_init_state ortac_postcond]) diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc index b90555f8..b5bfa7b4 100644 --- a/plugins/qcheck-stm/test/dune.inc +++ b/plugins/qcheck-stm/test/dune.inc @@ -32,7 +32,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm array) (action (echo @@ -85,7 +85,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm hashtbl) (action (echo @@ -138,7 +138,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm record) (action (echo @@ -191,7 +191,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm ref) (action (echo @@ -244,7 +244,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm conjunctive_clauses) (action (echo @@ -297,7 +297,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm sequence_model) (action (echo @@ -350,7 +350,7 @@ qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm invariants) (action (echo diff --git a/plugins/qcheck-stm/test/dune_gen.ml b/plugins/qcheck-stm/test/dune_gen.ml index e373efbf..57e5fe29 100644 --- a/plugins/qcheck-stm/test/dune_gen.ml +++ b/plugins/qcheck-stm/test/dune_gen.ml @@ -45,7 +45,7 @@ let rec print_rules pos = qcheck-stm.stm qcheck-stm.sequential qcheck-multicoretests-util - ortac-runtime + ortac-runtime-qcheck-stm %s) (action (echo diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml index e70df292..28756e00 100644 --- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Hashtbl +module Ortac_runtime = Ortac_runtime_qcheck_stm let rec remove_first x xs_1 = try match xs_1 with @@ -29,7 +31,6 @@ let rec remove_first x xs_1 = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = (char, int) t type cmd = | Clear @@ -259,193 +260,7 @@ module Spec = | Remove a_7 -> true | Replace (a_8, b_3) -> true | Length -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Clear, Res ((Unit, _), _)) -> true - | (Reset, Res ((Unit, _), _)) -> true - | (Add (a_2, b_2), Res ((Unit, _), _)) -> true - | (Find a_3, Res ((Result (Int, Exn), _), b_4)) -> - (match b_4 with - | Ok b_4 -> - (try - Ortac_runtime.Gospelstdlib.List.mem (a_3, b_4) - (Lazy.force new_state__007_).contents - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1372 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 32; - pos_bol = 1360; - pos_cnum = 1398 - } - }))) - | Error (Not_found) -> - (try - not - (Ortac_runtime.Gospelstdlib.List.mem a_3 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1317 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 31; - pos_bol = 1293; - pos_cnum = 1359 - } - }))) - | _ -> false) - | (Find_opt a_4, Res ((Option (Int), _), o)) -> - (try - (match o with - | None -> - if - not - (Ortac_runtime.Gospelstdlib.List.mem a_4 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - then true - else false - | Some b_5 -> - if - Ortac_runtime.Gospelstdlib.List.mem (a_4, b_5) - (Lazy.force new_state__007_).contents - then true - else false) - = true - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 36; - pos_bol = 1559; - pos_cnum = 1571 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 38; - pos_bol = 1643; - pos_cnum = 1687 - } - }))) - | (Find_all a_5, Res ((List (Int), _), bs)) -> - (try - (Ortac_runtime.Gospelstdlib.List.to_seq bs) = - (Ortac_runtime.Gospelstdlib.Sequence.filter_map - (fun (x_1, y) -> if x_1 = a_5 then Some y else None) - (Ortac_runtime.Gospelstdlib.List.to_seq - (Lazy.force new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1865 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 42; - pos_bol = 1853; - pos_cnum = 1947 - } - }))) - | (Mem a_6, Res ((Bool, _), b_6)) -> - (try - (b_6 = true) = - (Ortac_runtime.Gospelstdlib.List.mem a_6 - (Ortac_runtime.Gospelstdlib.List.map - Ortac_runtime.Gospelstdlib.fst - (Lazy.force new_state__007_).contents)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2161 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 46; - pos_bol = 2149; - pos_cnum = 2201 - } - }))) - | (Remove a_7, Res ((Unit, _), _)) -> true - | (Replace (a_8, b_3), Res ((Unit, _), _)) -> true - | (Length, Res ((Int, _), i)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i) = - (Ortac_runtime.Gospelstdlib.List.length - (Lazy.force new_state__007_).contents) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3739 - }; - Ortac_runtime.stop = - { - pos_fname = "hashtbl.mli"; - pos_lnum = 76; - pos_bol = 3727; - pos_cnum = 3765 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Clear -> Res (unit, (clear sut__011_)) @@ -460,12 +275,321 @@ module Spec = | Replace (a_8, b_3) -> Res (unit, (replace sut__011_ a_8 b_3)) | Length -> Res (int, (length sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Clear, Res ((Unit, _), _)) -> [] + | (Reset, Res ((Unit, _), _)) -> [] + | (Add (a_2, b_2), Res ((Unit, _), _)) -> [] + | (Find a_3, Res ((Result (Int, Exn), _), b_4)) -> + (match b_4 with + | Ok b_4 -> + if + (try + Ortac_runtime.Gospelstdlib.List.mem (a_3, b_4) + (Lazy.force new_state__007_).contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1372 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1398 + } + }))) + then [] + else + [("find", "List.mem (a, b) h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1372 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 32; + pos_bol = 1360; + pos_cnum = 1398 + } + })] + | Error (Not_found) -> + if + (try + not + (Ortac_runtime.Gospelstdlib.List.mem a_3 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1317 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1359 + } + }))) + then [] + else + [("find", "not (List.mem a (List.map fst h.contents))", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1317 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 31; + pos_bol = 1293; + pos_cnum = 1359 + } + })] + | _ -> []) + | (Find_opt a_4, Res ((Option (Int), _), o)) -> + if + (try + (match o with + | None -> + if + not + (Ortac_runtime.Gospelstdlib.List.mem a_4 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + then true + else false + | Some b_5 -> + if + Ortac_runtime.Gospelstdlib.List.mem (a_4, b_5) + (Lazy.force new_state__007_).contents + then true + else false) + = true + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 38; + pos_bol = 1643; + pos_cnum = 1687 + } + }))) + then [] + else + [("find_opt", + "match o with\n | None -> not (List.mem a (List.map fst h.contents))\n | Some b -> List.mem (a, b) h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 36; + pos_bol = 1559; + pos_cnum = 1571 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 38; + pos_bol = 1643; + pos_cnum = 1687 + } + })] + | (Find_all a_5, Res ((List (Int), _), bs)) -> + if + (try + (Ortac_runtime.Gospelstdlib.List.to_seq bs) = + (Ortac_runtime.Gospelstdlib.Sequence.filter_map + (fun (x_1, y) -> if x_1 = a_5 then Some y else None) + (Ortac_runtime.Gospelstdlib.List.to_seq + (Lazy.force new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1865 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1947 + } + }))) + then [] + else + [("find_all", + "bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1865 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 42; + pos_bol = 1853; + pos_cnum = 1947 + } + })] + | (Mem a_6, Res ((Bool, _), b_6)) -> + if + (try + (b_6 = true) = + (Ortac_runtime.Gospelstdlib.List.mem a_6 + (Ortac_runtime.Gospelstdlib.List.map + Ortac_runtime.Gospelstdlib.fst + (Lazy.force new_state__007_).contents)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2161 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2201 + } + }))) + then [] + else + [("mem", "b = List.mem a (List.map fst h.contents)", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2161 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 46; + pos_bol = 2149; + pos_cnum = 2201 + } + })] + | (Remove a_7, Res ((Unit, _), _)) -> [] + | (Replace (a_8, b_3), Res ((Unit, _), _)) -> [] + | (Length, Res ((Int, _), i)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int i) = + (Ortac_runtime.Gospelstdlib.List.length + (Lazy.force new_state__007_).contents) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3739 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3765 + } + }))) + then [] + else + [("length", "i = List.length h.contents", + { + Ortac_runtime.start = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3739 + }; + Ortac_runtime.stop = + { + pos_fname = "hashtbl.mli"; + pos_lnum = 76; + pos_bol = 3727; + pos_cnum = 3765 + } + })] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Hashtbl STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Hashtbl STM tests" wrapped_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml index cf3b1987..dac0389e 100644 --- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml @@ -1,8 +1,9 @@ +[@@@ocaml.warning "-26-27"] open Invariants +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = int t type cmd = | Push of int @@ -74,41 +75,11 @@ module Spec = } let precond cmd__008_ state__009_ = match cmd__008_ with | Push a_1 -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Push a_1, Res ((Unit, _), _)) -> - (try - Ortac_runtime.Gospelstdlib.(>) - (Ortac_runtime.Gospelstdlib.List.length - (Lazy.force new_state__007_).contents) - (Ortac_runtime.Gospelstdlib.integer_of_int 0) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "invariants.mli"; - pos_lnum = 4; - pos_bol = 110; - pos_cnum = 124 - }; - Ortac_runtime.stop = - { - pos_fname = "invariants.mli"; - pos_lnum = 4; - pos_bol = 110; - pos_cnum = 150 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Push a_1 -> Res (unit, (push a_1 sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = let __state__012_ = Spec.init_state in if @@ -139,10 +110,61 @@ let wrapped_init_state () = })) then __state__012_ else QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT" -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Push a_1, Res ((Unit, _), _)) -> + if + (try + Ortac_runtime.Gospelstdlib.(>) + (Ortac_runtime.Gospelstdlib.List.length + (Lazy.force new_state__007_).contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + }))) + then [] + else + [("push", "List.length x.contents > 0", + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + })] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Invariants STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Invariants STM tests" + wrapped_init_state ortac_postcond]) diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml index b590e44e..650c50fb 100644 --- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Record +module Ortac_runtime = Ortac_runtime_qcheck_stm let plus1_1 i = try Ortac_runtime.Gospelstdlib.(+) i @@ -27,7 +29,6 @@ let plus1_1 i = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = t type cmd = | Get @@ -70,102 +71,164 @@ module Spec = let next_state cmd__002_ state__003_ = match cmd__002_ with | Get -> state__003_ let precond cmd__008_ state__009_ = match cmd__008_ with | Get -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Get, Res ((Int, _), i_1)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) = - (Lazy.force new_state__007_).value - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "record.mli"; - pos_lnum = 23; - pos_bol = 868; - pos_cnum = 880 - }; - Ortac_runtime.stop = - { - pos_fname = "record.mli"; - pos_lnum = 23; - pos_bol = 868; - pos_cnum = 891 - } - }))) - && - ((try - (plus1_1 (Ortac_runtime.Gospelstdlib.integer_of_int i_1)) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int 1)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "record.mli"; - pos_lnum = 25; - pos_bol = 912; - pos_cnum = 924 - }; - Ortac_runtime.stop = - { - pos_fname = "record.mli"; - pos_lnum = 25; - pos_bol = 912; - pos_cnum = 939 - } - }))) - && - ((try - (Ortac_runtime.Gospelstdlib.integer_of_int (plus2 i_1)) = - (Ortac_runtime.Gospelstdlib.(+) - (Ortac_runtime.Gospelstdlib.integer_of_int i_1) - (Ortac_runtime.Gospelstdlib.integer_of_int 2)) - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "record.mli"; - pos_lnum = 26; - pos_bol = 940; - pos_cnum = 952 - }; - Ortac_runtime.stop = - { - pos_fname = "record.mli"; - pos_lnum = 26; - pos_bol = 940; - pos_cnum = 967 - } - }))))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Get -> Res (int, (get sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = let __state__012_ = Spec.init_state in if true then __state__012_ else QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT" -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Get, Res ((Int, _), i_1)) -> + (if + try + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) = + (Lazy.force new_state__007_).value + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 880 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 891 + } + })) + then [] + else + [("get", "i = r.value", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 880 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 23; + pos_bol = 868; + pos_cnum = 891 + } + })]) + @ + ((if + try + (plus1_1 (Ortac_runtime.Gospelstdlib.integer_of_int i_1)) = + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int 1)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 924 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 939 + } + })) + then [] + else + [("get", "plus1 i = i + 1", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 924 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 25; + pos_bol = 912; + pos_cnum = 939 + } + })]) + @ + (if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int (plus2 i_1)) + = + (Ortac_runtime.Gospelstdlib.(+) + (Ortac_runtime.Gospelstdlib.integer_of_int i_1) + (Ortac_runtime.Gospelstdlib.integer_of_int 2)) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 952 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 967 + } + }))) + then [] + else + [("get", "plus2 i = i + 2", + { + Ortac_runtime.start = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 952 + }; + Ortac_runtime.stop = + { + pos_fname = "record.mli"; + pos_lnum = 26; + pos_bol = 940; + pos_cnum = 967 + } + })])) + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Record STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Record STM tests" wrapped_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml index 5c475d16..d48b7e4f 100644 --- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml @@ -1,8 +1,9 @@ +[@@@ocaml.warning "-26-27"] open Ref +module Ortac_runtime = Ortac_runtime_qcheck_stm module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = t type cmd = | Get @@ -45,44 +46,65 @@ module Spec = let next_state cmd__002_ state__003_ = match cmd__002_ with | Get -> state__003_ let precond cmd__008_ state__009_ = match cmd__008_ with | Get -> true - let postcond cmd__004_ state__005_ res__006_ = - let new_state__007_ = lazy (next_state cmd__004_ state__005_) in - match (cmd__004_, res__006_) with - | (Get, Res ((Int, _), i)) -> - (try - (Ortac_runtime.Gospelstdlib.integer_of_int i) = - (Lazy.force new_state__007_).value - with - | e -> - raise - (Ortac_runtime.Partial_function - (e, - { - Ortac_runtime.start = - { - pos_fname = "ref.mli"; - pos_lnum = 11; - pos_bol = 346; - pos_cnum = 358 - }; - Ortac_runtime.stop = - { - pos_fname = "ref.mli"; - pos_lnum = 11; - pos_bol = 346; - pos_cnum = 369 - } - }))) - | _ -> true + let postcond _ _ _ = true let run cmd__010_ sut__011_ = match cmd__010_ with | Get -> Res (int, (get sut__011_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__004_ state__005_ res__006_ = + let open Spec in + let open STM in + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Get, Res ((Int, _), i)) -> + if + (try + (Ortac_runtime.Gospelstdlib.integer_of_int i) = + (Lazy.force new_state__007_).value + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 358 + }; + Ortac_runtime.stop = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 369 + } + }))) + then [] + else + [("get", "i = r.value", + { + Ortac_runtime.start = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 358 + }; + Ortac_runtime.stop = + { + pos_fname = "ref.mli"; + pos_lnum = 11; + pos_bol = 346; + pos_cnum = 369 + } + })] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Ref STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Ref STM tests" wrapped_init_state + ortac_postcond]) diff --git a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml index 92bfa53a..b45016ec 100644 --- a/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/sequence_model_stm_tests.expected.ml @@ -1,4 +1,6 @@ +[@@@ocaml.warning "-26-27"] open Sequence_model +module Ortac_runtime = Ortac_runtime_qcheck_stm let length_opt s = try Some (Ortac_runtime.Gospelstdlib.Sequence.length s) with @@ -25,7 +27,6 @@ let length_opt s = module Spec = struct open STM - [@@@ocaml.warning "-26-27"] type sut = char t type cmd = | Add of char @@ -175,25 +176,26 @@ module Spec = } let precond cmd__010_ state__011_ = match cmd__010_ with | Add v -> true | Remove -> true | Remove_ -> true - let postcond cmd__006_ state__007_ res__008_ = - let new_state__009_ = lazy (next_state cmd__006_ state__007_) in - match (cmd__006_, res__008_) with - | (Add v, Res ((Unit, _), _)) -> true - | (Remove, Res ((Option (Char), _), o)) -> true - | (Remove_, Res ((Option (Char), _), o_1)) -> true - | _ -> true + let postcond _ _ _ = true let run cmd__012_ sut__013_ = match cmd__012_ with | Add v -> Res (unit, (add v sut__013_)) | Remove -> Res ((option char), (remove sut__013_)) | Remove_ -> Res ((option char), (remove_ sut__013_)) end -module STMTests = (STM_sequential.Make)(Spec) +module STMTests = (Ortac_runtime.Make)(Spec) let wrapped_init_state () = Spec.init_state -let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let ortac_postcond cmd__006_ state__007_ res__008_ = + let open Spec in + let open STM in + let new_state__009_ = lazy (next_state cmd__006_ state__007_) in + match (cmd__006_, res__008_) with + | (Add v, Res ((Unit, _), _)) -> [] + | (Remove, Res ((Option (Char), _), o)) -> [] + | (Remove_, Res ((Option (Char), _), o_1)) -> [] + | _ -> [] let _ = - let open QCheck in - QCheck_base_runner.run_tests_main - (let count = 1000 in - [Test.make ~count ~name:"Sequence_model STM tests" - (STMTests.arb_cmds Spec.init_state) agree_prop]) + QCheck_base_runner.run_tests_main + (let count = 1000 in + [STMTests.agree_test ~count ~name:"Sequence_model STM tests" + wrapped_init_state ortac_postcond]) diff --git a/src/runtime/ortac_runtime_intf.ml b/src/runtime/ortac_runtime_intf.ml index 04c4e351..64dfa74c 100644 --- a/src/runtime/ortac_runtime_intf.ml +++ b/src/runtime/ortac_runtime_intf.ml @@ -22,6 +22,7 @@ module type S = sig mutable errors : error list; } + val pp_loc : Format.formatter -> location -> unit val pp_error_report : Format.formatter -> error_report -> unit exception Error of error_report