Module STM_domain.Make

check_obs pref cs1 cs2 s tests whether the observations from the sequential prefix pref and the parallel traces cs1 cs2 agree with the model started in state s.

all_interleavings_ok (seq,spawn0,spawn1) checks that preconditions of all the cmds of seq, spawn0, and spawn1 are satisfied in all the possible interleavings and starting with Spec.init_state. all_interleavings_ok catches and ignores exceptions arising from next_state.

arb_cmds_triple seq_len par_len generates a cmd triple with at most seq_len sequential commands and at most par_len parallel commands each. All cmds are generated with Spec.arb_cmd. arb_cmds_triple catches and ignores generation-time exceptions arising from Spec.next_state.

arb_triple seq_len par_len arb0 arb1 arb2 generates a cmd triple with at most seq_len sequential commands and at most par_len parallel commands each. The three Spec.cmd components are generated with arb0, arb1, and arb2, respectively. Each of these take the model state as a parameter. arb_triple catches and ignores generation-time exceptions arising from Spec.next_state.

arb_triple_asym seq_len par_len arb0 arb1 arb2 creates a triple cmd generator like arb_triple. It differs in that the resulting printer is asymmetric, printing arb1's result below arb0's result and printing arb2's result to the right of arb1's result. arb_triple_asym catches and ignores generation-time exceptions arising from Spec.next_state.

interp_sut_res sut cs interprets the commands cs over the system Spec.sut and returns the list of corresponding Spec.cmd and result pairs.

Parallel stress testing property based on Stdlib.Domain. stress_prop_par (seq_pref, tl1, tl2) first interprets seq_pref and then spawns two parallel, symmetric domains interpreting tl1 and tl2 simultaneously. In contrast to agree_prop_par, stress_prop_par does not perform an interleaving search.

• returns

  true if no unexpected exceptions or crashes are encountered.

Parallel agreement property based on Stdlib.Domain. agree_prop_par (seq_pref, tl1, tl2) first interprets seq_pref and then spawns two parallel, symmetric domains interpreting tl1 and tl2 simultaneously.

• returns

  true if there exists a sequential interleaving of the results which agrees with a model interpretation.

Asymmetric parallel agreement property based on Stdlib.Domain. agree_prop_par_asym (seq_pref, tl1, tl2) first interprets seq_pref, and then interprets tl1 while a spawned domain interprets tl2 in parallel with the parent domain.

• returns

  true if there exists a sequential interleaving of the results which agrees with a model interpretation.

Parallel agreement test based on Stdlib.Domain which combines repeat and ~retries. Accepts two labeled parameters: count is the number of test iterations and name is the printed test name.

A negative parallel agreement test (for convenience). Accepts two labeled parameters: count is the number of test iterations and name is the printed test name.

Asymmetric parallel agreement test based on Stdlib.Domain and agree_prop_par_asym which combines repeat and ~retries. Accepts two labeled parameters: count is the number of test iterations and name is the printed test name.

A negative asymmetric parallel agreement test (for convenience). Accepts two labeled parameters: count is the number of test iterations and name is the printed test name.

Parallel stress test based on Stdlib.Domain which combines repeat and ~retries. Accepts two labeled parameters: count is the number of test iterations and name is the printed test name. The test fails if an unexpected exception is raised underway. It is intended as a stress test to run operations at a high frequency and detect unexpected exceptions or crashes. It does not perform an interleaving search like agree_test_par and neg_agree_test_par.