forked from ocaml-gospel/ortac
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
177 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
type ('a, 'b) t = ('a, 'b) Hashtbl.t | ||
|
||
let empty () = Hashtbl.create 42 | ||
let add = Hashtbl.add |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
type ('a, 'b) t | ||
(*@ mutable model m : 'a -> 'b option *) | ||
|
||
val empty : unit -> ('a, 'b) t | ||
(*@ t = empty () | ||
ensures t.m = fun _ -> None *) | ||
|
||
val add : ('a, 'b) t -> 'a -> 'b -> unit | ||
(*@ add t a b | ||
modifies t.m | ||
ensures t.m = fun x -> if x = a then Some b else (old t.m) x *) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
type sut = (char, int) t | ||
|
||
let init_sut = empty () |
Empty file.
103 changes: 103 additions & 0 deletions
103
plugins/qcheck-stm/test/functional_model_stm_tests.expected.ml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,103 @@ | ||
(* This file is generated by ortac qcheck-stm, | ||
edit how you run the tool instead *) | ||
[@@@ocaml.warning "-26-27-69"] | ||
open Functional_model | ||
module Ortac_runtime = Ortac_runtime_qcheck_stm | ||
module Spec = | ||
struct | ||
open STM | ||
type sut = (char, int) t | ||
type cmd = | ||
| Add of char * int | ||
let show_cmd cmd__001_ = | ||
match cmd__001_ with | ||
| Add (a_1, b_1) -> | ||
Format.asprintf "%s sut %a %a" "add" (Util.Pp.pp_char true) a_1 | ||
(Util.Pp.pp_int true) b_1 | ||
type nonrec state = { | ||
m: char -> int option } | ||
let init_state = | ||
let () = () in | ||
{ | ||
m = | ||
(try fun _ -> None | ||
with | ||
| e -> | ||
raise | ||
(Ortac_runtime.Partial_function | ||
(e, | ||
{ | ||
Ortac_runtime.start = | ||
{ | ||
pos_fname = "functional_model.mli"; | ||
pos_lnum = 6; | ||
pos_bol = 275; | ||
pos_cnum = 293 | ||
}; | ||
Ortac_runtime.stop = | ||
{ | ||
pos_fname = "functional_model.mli"; | ||
pos_lnum = 6; | ||
pos_bol = 275; | ||
pos_cnum = 306 | ||
} | ||
}))) | ||
} | ||
let init_sut () = empty () | ||
let cleanup _ = () | ||
let arb_cmd _ = | ||
let open QCheck in | ||
make ~print:show_cmd | ||
(let open Gen in | ||
oneof | ||
[((pure (fun a_1 -> fun b_1 -> Add (a_1, b_1))) <*> char) <*> | ||
int]) | ||
let next_state cmd__002_ state__003_ = | ||
match cmd__002_ with | ||
| Add (a_1, b_1) -> | ||
{ | ||
m = | ||
((try fun x -> if x = a_1 then Some b_1 else state__003_.m x | ||
with | ||
| e -> | ||
raise | ||
(Ortac_runtime.Partial_function | ||
(e, | ||
{ | ||
Ortac_runtime.start = | ||
{ | ||
pos_fname = "functional_model.mli"; | ||
pos_lnum = 11; | ||
pos_bol = 482; | ||
pos_cnum = 500 | ||
}; | ||
Ortac_runtime.stop = | ||
{ | ||
pos_fname = "functional_model.mli"; | ||
pos_lnum = 11; | ||
pos_bol = 482; | ||
pos_cnum = 546 | ||
} | ||
})))) | ||
} | ||
let precond cmd__008_ state__009_ = | ||
match cmd__008_ with | Add (a_1, b_1) -> true | ||
let postcond _ _ _ = true | ||
let run cmd__010_ sut__011_ = | ||
match cmd__010_ with | ||
| Add (a_1, b_1) -> Res (unit, (add sut__011_ a_1 b_1)) | ||
end | ||
module STMTests = (Ortac_runtime.Make)(Spec) | ||
let check_init_state () = () | ||
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 | ||
| (Add (a_1, b_1), Res ((Unit, _), _)) -> None | ||
| _ -> None | ||
let _ = | ||
QCheck_base_runner.run_tests_main | ||
(let count = 1000 in | ||
[STMTests.agree_test ~count ~name:"Functional_model STM tests" | ||
check_init_state ortac_postcond]) |