From 0d73b1e562d5998a0a6002d23ccdcc049069a632 Mon Sep 17 00:00:00 2001 From: Fabian Vu <Fabian.Vu@hhu.de> Date: Sun, 24 Nov 2024 22:54:02 +0100 Subject: [PATCH] Update information about models --- benchmarks/code_gen/LandingGear_R6.mch | 6 + benchmarks/code_gen/sort_m2_data1000_MC.mch | 4 + .../execution/ProB/sort_m2_data1000.mch | 4 + .../ProB/sort_m2_data1000_asserts.mch | 5 +- .../ProB/sort_m2_data1000_asserts_exec.mch | 4 + .../model_checking/ProB/LandingGear_R6.mch | 6 + .../ProB/Train_1_beebook_tlc_POR.mch | 183 +++++++++++ .../ProB/sort_m2_data1000_MC.mch | 4 + .../model_checking/TLC/LandingGear_R6.mch | 6 + .../ProB/LandingGear_R6.mch | 6 + ...rain_1_beebook_deterministic_MC_POR_v3.mch | 178 +++++++++++ .../model_checking_opreuse/ProB/nota_v2.mch | 300 ++++++++++++++++++ .../ProB/prob_oneway8seq.mch | 3 + .../ProB/sort_m2_data1000_MC.mch | 4 + .../TLC/LandingGear_R6.mch | 6 + .../model_checking_opreuse/TLC/nota_v2.mch | 300 ++++++++++++++++++ .../TLC/prob_oneway8seq.mch | 4 +- .../TLC/prob_oneway8seq_tlc.mch | 5 +- 18 files changed, 1025 insertions(+), 3 deletions(-) create mode 100644 benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch create mode 100644 benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch create mode 100644 benchmarks/model_checking_opreuse/ProB/nota_v2.mch create mode 100644 benchmarks/model_checking_opreuse/TLC/nota_v2.mch diff --git a/benchmarks/code_gen/LandingGear_R6.mch b/benchmarks/code_gen/LandingGear_R6.mch index 72bd1819e..0c757ca06 100644 --- a/benchmarks/code_gen/LandingGear_R6.mch +++ b/benchmarks/code_gen/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/benchmarks/code_gen/sort_m2_data1000_MC.mch b/benchmarks/code_gen/sort_m2_data1000_MC.mch index 13d764409..b932db0c1 100644 --- a/benchmarks/code_gen/sort_m2_data1000_MC.mch +++ b/benchmarks/code_gen/sort_m2_data1000_MC.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_MC // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/benchmarks/execution/ProB/sort_m2_data1000.mch b/benchmarks/execution/ProB/sort_m2_data1000.mch index 92ae1adfd..c2c3351c9 100644 --- a/benchmarks/execution/ProB/sort_m2_data1000.mch +++ b/benchmarks/execution/ProB/sort_m2_data1000.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000 // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/benchmarks/execution/ProB/sort_m2_data1000_asserts.mch b/benchmarks/execution/ProB/sort_m2_data1000_asserts.mch index 16db461ab..2e9c28957 100644 --- a/benchmarks/execution/ProB/sort_m2_data1000_asserts.mch +++ b/benchmarks/execution/ProB/sort_m2_data1000_asserts.mch @@ -1,4 +1,7 @@ - +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_asserts DEFINITIONS GOAL == k = n CONCRETE_CONSTANTS diff --git a/benchmarks/execution/ProB/sort_m2_data1000_asserts_exec.mch b/benchmarks/execution/ProB/sort_m2_data1000_asserts_exec.mch index ebd2109f6..cdc1cc3fb 100644 --- a/benchmarks/execution/ProB/sort_m2_data1000_asserts_exec.mch +++ b/benchmarks/execution/ProB/sort_m2_data1000_asserts_exec.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_asserts_exec INCLUDES sort_m2_data1000_asserts diff --git a/benchmarks/model_checking/ProB/LandingGear_R6.mch b/benchmarks/model_checking/ProB/LandingGear_R6.mch index 72bd1819e..0c757ca06 100644 --- a/benchmarks/model_checking/ProB/LandingGear_R6.mch +++ b/benchmarks/model_checking/ProB/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch b/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch new file mode 100644 index 000000000..6cc273050 --- /dev/null +++ b/benchmarks/model_checking/ProB/Train_1_beebook_tlc_POR.mch @@ -0,0 +1,183 @@ +MACHINE Train_1_beebook_tlc_POR +SETS /* enumerated */ + BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; + ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10} +DEFINITIONS + ROUTE_FREEING_IMPOSSIBLE == ({} = resrt \ ran(rsrtbl)) +CONCRETE_CONSTANTS + fst, + lst, + nxt, + rtbl +ABSTRACT_VARIABLES + LBT, + TRK, + frm, + OCC, + resbl, + resrt, + rsrtbl +/* PROMOTED OPERATIONS + route_reservation, + route_freeing, + FRONT_MOVE_1, + FRONT_MOVE_2, + BACK_MOVE_1, + BACK_MOVE_2, + point_positionning, + route_formation */ +PROPERTIES + /* @axm2 */ dom(rtbl) = BLOCKS + & /* @axm3 */ ran(rtbl) = ROUTES + & /* @axm4 */ nxt : ROUTES --> (BLOCKS >+> BLOCKS) + & /* @axm5 */ fst : ROUTES --> BLOCKS + & /* @axm6 */ lst : ROUTES --> BLOCKS + & /* @axm7 */ fst~ <: rtbl + & /* @axm8 */ lst~ <: rtbl + & /* @axm11 */ !(r).(r : ROUTES => fst(r) /= lst(r)) + & /* @axm10 */ !(r).(r : ROUTES => !(S).(S <: ran(nxt(r)) & S <: nxt(r)[S] => S = {})) + & /* @axm9 */ !(r).(r : ROUTES => nxt(r) : (rtbl~)[{r}] \ {lst(r)} >->> (rtbl~)[{r}] \ {fst(r)}) + & /* @axm12 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => fst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)}) + & /* @axm13 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => lst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)}) + & /* @compute_rtbl_from_nxt */ rtbl = {b,r|b : BLOCKS & (r : dom(nxt) & (b : dom(nxt(r)) or b : ran(nxt(r))))} + & /* @axm40 */ nxt = {R1 |-> {L |-> A,A |-> B,B |-> C},R2 |-> {L |-> A,A |-> B,B |-> D,D |-> E,E |-> F,F |-> G},R3 |-> {L |-> A,A |-> B,B |-> D,D |-> K,K |-> J,J |-> N},R4 |-> {M |-> H,H |-> I,I |-> K,K |-> F,F |-> G},R5 |-> {M |-> H,H |-> I,I |-> J,J |-> N},R6 |-> {C |-> B,B |-> A,A |-> L},R7 |-> {G |-> F,F |-> E,E |-> D,D |-> B,B |-> A,A |-> L},R8 |-> {N |-> J,J |-> K,K |-> D,D |-> B,B |-> A,A |-> L},R9 |-> {G |-> F,F |-> K,K |-> I,I |-> H,H |-> M},R10 |-> {N |-> J,J |-> I,I |-> H,H |-> M}} + & /* @axm41 */ fst = {R1 |-> L,R2 |-> L,R3 |-> L,R4 |-> M,R5 |-> M,R6 |-> C,R7 |-> G,R8 |-> N,R9 |-> G,R10 |-> N} + & /* @axm42 */ lst = {R1 |-> C,R2 |-> G,R3 |-> N,R4 |-> G,R5 |-> N,R6 |-> L,R7 |-> L,R8 |-> L,R9 |-> M,R10 |-> M} +INVARIANT + /* @inv3 */ rsrtbl : resbl --> resrt + & /* @inv5 */ rsrtbl <: rtbl + & /* @inv4 */ OCC <: resbl + & /* @inv6 */ !(r).(r : ROUTES => nxt(r)[(rtbl~)[{r}] \ (rsrtbl~)[{r}]] /\ (rsrtbl~)[{r}] \ OCC = {}) + & /* @inv7 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}]] <: (rsrtbl~)[{r}]) + & /* @inv8 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}] \ OCC] <: (rsrtbl~)[{r}] \ OCC) + & /* @inv1 */ TRK : BLOCKS >+> BLOCKS + & /* @inv2 */ frm <: resrt + & /* @inv3 */ rsrtbl[OCC] <: frm + & /* @inv4 */ !(r).(r : resrt \ frm => rtbl |> {r} = rsrtbl |> {r}) + & /* @inv5 */ !(x,y).((x : BLOCKS & y : BLOCKS) & x |-> y : TRK => #(r).(r : ROUTES & x |-> y : nxt(r))) + & /* @inv6 */ !(r).(r : frm => (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK) + & /* @inv7 */ LBT <: OCC + & /* @inv8 */ !(a,b).(b : LBT & (b : ran(nxt(rsrtbl(b))) & (a = (nxt(rsrtbl(b))~)(b) & a : dom(rsrtbl))) => rsrtbl(a) /= rsrtbl(b)) + +ASSERTIONS + /* @thm1 */ !(b).(b : OCC & b : dom(TRK) => nxt(rsrtbl(b))(b) = TRK(b)); + /* @thm2 */ ran(lst) /\ dom(TRK) \ ran(fst) = {}; + /* @thm3 */ ran(fst) /\ ran(TRK) \ ran(lst) = {} +INITIALISATION + resrt := {} + || + resbl := {} + || + rsrtbl := {} + || + OCC := {} + || + TRK := {} + || + frm := {} + || + LBT := {} + +OPERATIONS + route_reservation = + + ANY r + WHERE + /* @grd1 */ r /: resrt + & /* @grd2 */ (rtbl~)[{r}] /\ resbl = {} + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + resrt := resrt \/ {r} + || + rsrtbl := rsrtbl \/ (rtbl |> {r}) + || + resbl := resbl \/ (rtbl~)[{r}] + END; + + route_freeing = + ANY r + WHERE + /* @grd1 */ r : resrt \ ran(rsrtbl) + THEN + resrt := resrt \ {r} + || + frm := frm \ {r} + END; + + FRONT_MOVE_1 = + ANY r + WHERE + /* @grd1 */ r : frm + & /* @grd2 */ fst(r) : resbl \ OCC + & /* @grd3 */ rsrtbl(fst(r)) = r + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + OCC := OCC \/ {fst(r)} + || + LBT := LBT \/ {fst(r)} + END; + + FRONT_MOVE_2 = + ANY b + WHERE + /* @grd1 */ b : OCC + & /* @grd2 */ b : dom(TRK) + & /* @grd3 */ TRK(b) /: OCC + THEN + OCC := OCC \/ {TRK(b)} + END; + + BACK_MOVE_1 = + ANY b + WHERE + /* @grd1 */ b : LBT + & /* @grd2 */ b /: dom(TRK) + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + OCC := OCC \ {b} + || + rsrtbl := {b} <<| rsrtbl + || + resbl := resbl \ {b} + || + LBT := LBT \ {b} + END; + + BACK_MOVE_2 = + ANY b + WHERE + /* @grd1 */ b : LBT + & /* @grd2 */ b : dom(TRK) + & /* @grd3 */ TRK(b) : OCC + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + OCC := OCC \ {b} + || + rsrtbl := {b} <<| rsrtbl + || + resbl := resbl \ {b} + || + LBT := LBT \ {b} \/ {TRK(b)} + + END; + + point_positionning = + ANY r + WHERE + /* @grd1 */ r : resrt \ frm + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + TRK := ((dom(nxt(r)) <<| TRK) |>> ran(nxt(r))) \/ nxt(r) + END; + + route_formation = + ANY r + WHERE + /* @grd1 */ r : resrt \ frm + & /* @grd2 */ (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK + & ROUTE_FREEING_IMPOSSIBLE /* POR REDUCTION */ + THEN + frm := frm \/ {r} + END +END + diff --git a/benchmarks/model_checking/ProB/sort_m2_data1000_MC.mch b/benchmarks/model_checking/ProB/sort_m2_data1000_MC.mch index 380ad9898..69eb867bd 100644 --- a/benchmarks/model_checking/ProB/sort_m2_data1000_MC.mch +++ b/benchmarks/model_checking/ProB/sort_m2_data1000_MC.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_MC // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/benchmarks/model_checking/TLC/LandingGear_R6.mch b/benchmarks/model_checking/TLC/LandingGear_R6.mch index 72bd1819e..0c757ca06 100644 --- a/benchmarks/model_checking/TLC/LandingGear_R6.mch +++ b/benchmarks/model_checking/TLC/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/benchmarks/model_checking_opreuse/ProB/LandingGear_R6.mch b/benchmarks/model_checking_opreuse/ProB/LandingGear_R6.mch index 72bd1819e..0c757ca06 100644 --- a/benchmarks/model_checking_opreuse/ProB/LandingGear_R6.mch +++ b/benchmarks/model_checking_opreuse/ProB/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch new file mode 100644 index 000000000..4a4d10182 --- /dev/null +++ b/benchmarks/model_checking_opreuse/ProB/Train_1_beebook_deterministic_MC_POR_v3.mch @@ -0,0 +1,178 @@ +MACHINE Train_1_beebook_deterministic_MC_POR_v3 // this version is very close to Train_1_beebook_tlc_POR. For instance, top-level ANY substitutions are not re-written to PRE as done in Train_1_beebook_deterministic_MC_POR_v2. DEFINITIONS are still inlined. +SETS /* enumerated */ + BLOCKS={A,B,C,D,E,F,G,H,I,J,K,L,M,N}; + ROUTES={R1,R2,R3,R4,R5,R6,R7,R8,R9,R10} +CONCRETE_CONSTANTS + fst, + lst, + nxt, + rtbl +ABSTRACT_VARIABLES + LBT, + TRK, + frm, + OCC, + resbl, + resrt, + rsrtbl +/* PROMOTED OPERATIONS + route_reservation, + route_freeing, + FRONT_MOVE_1, + FRONT_MOVE_2, + BACK_MOVE_1, + BACK_MOVE_2, + point_positionning, + route_formation */ +PROPERTIES + /* @axm2 */ dom(rtbl) = BLOCKS + & /* @axm3 */ ran(rtbl) = ROUTES + & /* @axm4 */ dom(nxt) = ROUTES & ran(nxt) <: (BLOCKS >+> BLOCKS) + & /* @axm5 */ fst : ROUTES --> BLOCKS + & /* @axm6 */ lst : ROUTES --> BLOCKS + & /* @axm7 */ fst~ <: rtbl + & /* @axm8 */ lst~ <: rtbl + & /* @axm11 */ !(r).(r : ROUTES => fst(r) /= lst(r)) + & /* @axm10 */ !(r).(r : ROUTES => !(S).(S <: ran(nxt(r)) & S <: nxt(r)[S] => S = {})) + & /* @axm9 */ !(r).(r : ROUTES => nxt(r) : (rtbl~)[{r}] \ {lst(r)} >->> (rtbl~)[{r}] \ {fst(r)}) + & /* @axm12 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => fst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)}) + & /* @axm13 */ !(r,s).((r : ROUTES & s : ROUTES) & r /= s => lst(r) /: (rtbl~)[{s}] \ {fst(s),lst(s)}) + & /* @compute_rtbl_from_nxt */ rtbl = {b,r|b : BLOCKS & r : ROUTES & (r : dom(nxt) & (b : dom(nxt(r)) or b : ran(nxt(r))))} + & /* @axm40 */ nxt = {R1 |-> {L |-> A,A |-> B,B |-> C},R2 |-> {L |-> A,A |-> B,B |-> D,D |-> E,E |-> F,F |-> G},R3 |-> {L |-> A,A |-> B,B |-> D,D |-> K,K |-> J,J |-> N},R4 |-> {M |-> H,H |-> I,I |-> K,K |-> F,F |-> G},R5 |-> {M |-> H,H |-> I,I |-> J,J |-> N},R6 |-> {C |-> B,B |-> A,A |-> L},R7 |-> {G |-> F,F |-> E,E |-> D,D |-> B,B |-> A,A |-> L},R8 |-> {N |-> J,J |-> K,K |-> D,D |-> B,B |-> A,A |-> L},R9 |-> {G |-> F,F |-> K,K |-> I,I |-> H,H |-> M},R10 |-> {N |-> J,J |-> I,I |-> H,H |-> M}} + & /* @axm41 */ fst = {R1 |-> L,R2 |-> L,R3 |-> L,R4 |-> M,R5 |-> M,R6 |-> C,R7 |-> G,R8 |-> N,R9 |-> G,R10 |-> N} + & /* @axm42 */ lst = {R1 |-> C,R2 |-> G,R3 |-> N,R4 |-> G,R5 |-> N,R6 |-> L,R7 |-> L,R8 |-> L,R9 |-> M,R10 |-> M} +INVARIANT + /* @inv3 */ rsrtbl : resbl --> resrt + & /* @inv5 */ rsrtbl <: rtbl + & /* @inv4 */ OCC <: resbl + & /* @inv6 */ !(r).(r : ROUTES => nxt(r)[(rtbl~)[{r}] \ (rsrtbl~)[{r}]] /\ (rsrtbl~)[{r}] \ OCC = {}) + & /* @inv7 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}]] <: (rsrtbl~)[{r}]) + & /* @inv8 */ !(r).(r : ROUTES => nxt(r)[(rsrtbl~)[{r}] \ OCC] <: (rsrtbl~)[{r}] \ OCC) + & /* @inv1 */ TRK : BLOCKS >+> BLOCKS + & /* @inv2 */ frm <: resrt + & /* @inv3 */ rsrtbl[OCC] <: frm + & /* @inv4 */ !(r).(r : resrt \ frm => rtbl |> {r} = rsrtbl |> {r}) + & /* @inv5 */ !(x,y).(x : BLOCKS & y : BLOCKS & x |-> y : TRK => #(r).(r : ROUTES & x |-> y : nxt(r))) + & /* @inv6 */ !(r).(r : frm => (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK) + & /* @inv7 */ LBT <: OCC + & /* @inv8 */ !(a,b).(a : BLOCKS & b : LBT & (b : ran(nxt(rsrtbl(b))) & (a = (nxt(rsrtbl(b))~)(b) & a : dom(rsrtbl))) => rsrtbl(a) /= rsrtbl(b)) +ASSERTIONS + /* @thm1 */ !(b).(b : OCC & b : dom(TRK) => nxt(rsrtbl(b))(b) = TRK(b)); + /* @thm2 */ ran(lst) /\ dom(TRK) \ ran(fst) = {}; + /* @thm3 */ ran(fst) /\ ran(TRK) \ ran(lst) = {} +INITIALISATION + resrt := {} + || + resbl := {} + || + rsrtbl := {} + || + OCC := {} + || + TRK := {} + || + frm := {} + || + LBT := {} + +OPERATIONS + route_reservation = + + ANY r + WHERE + /* @grd1 */ r : ROUTES \ resrt + & /* @grd2 */ (rtbl~)[{r}] /\ resbl = {} + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + resrt := resrt \/ {r} + || + rsrtbl := rsrtbl \/ (rtbl |> {r}) + || + resbl := resbl \/ (rtbl~)[{r}] + END; + + route_freeing = + ANY r + WHERE + /* @grd1 */ r : resrt \ ran(rsrtbl) + THEN + resrt := resrt \ {r} + || + frm := frm \ {r} + END; + + FRONT_MOVE_1 = + ANY r + WHERE + /* @grd1 */ r : frm + & /* @grd3 */ fst(r) : resbl \ OCC + & /* @grd2 */ r = rsrtbl(fst(r)) + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + OCC := OCC \/ {fst(r)} + || + LBT := LBT \/ {fst(r)} + END; + + FRONT_MOVE_2 = + ANY b + WHERE + /* @grd1 */ b : OCC /\ dom(TRK) + & /* @grd2 */ TRK(b) /: OCC + THEN + OCC := OCC \/ {TRK(b)} + END; + + BACK_MOVE_1 = + ANY b + WHERE + /* @grd1 */ b : LBT \ dom(TRK) + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + OCC := OCC \ {b} + || + rsrtbl := {b} <<| rsrtbl + || + resbl := resbl \ {b} + || + LBT := LBT \ {b} + END; + + BACK_MOVE_2 = + ANY b + WHERE + /* @grd1 */ b : LBT /\ dom(TRK) + & /* @grd2 */ TRK(b) : OCC + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + OCC := OCC \ {b} + || + rsrtbl := {b} <<| rsrtbl + || + resbl := resbl \ {b} + || + LBT := LBT \ {b} \/ {TRK(b)} + + END; + + point_positionning = + ANY r + WHERE + /* @grd1 */ r : resrt \ frm + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + TRK := ((dom(nxt(r)) <<| TRK) |>> ran(nxt(r))) \/ nxt(r) + END; + + route_formation = + ANY r + WHERE + /* @grd1 */ r : resrt \ frm + & /* @grd2 */ (rsrtbl~)[{r}] <| nxt(r) = (rsrtbl~)[{r}] <| TRK + & ({} = resrt \ ran(rsrtbl)) /* POR REDUCTION */ + THEN + frm := frm \/ {r} + END + +END + diff --git a/benchmarks/model_checking_opreuse/ProB/nota_v2.mch b/benchmarks/model_checking_opreuse/ProB/nota_v2.mch new file mode 100644 index 000000000..62b04c894 --- /dev/null +++ b/benchmarks/model_checking_opreuse/ProB/nota_v2.mch @@ -0,0 +1,300 @@ +MACHINE nota_v2 +// a simplified version of nota for B2Program + +/* these represent the classes */ +/* effectively these also include their addresses, which in an + OO context in their object ID. Note that also SERVICE also + includes the properties of those service objects, ie: the ID of + a service is more complicated than just an object id */ + + +SETS + INTERCONNECTNODE = {node1,node2}; + SOCKET = {socket1,socket2}; + SERVICE = {service1,service2}; + RESOURCEMANAGER = {resource1,resource2}; + SID = {SID1,SID2}; + +/* error codes */ + RM_ERROR_CODES = { RM_SERVICE_FOUND, RM_SERVICE_NOT_FOUND } ; + IN_ERROR_CODES = { IN_REGISTRATION_OK, IN_REGISTRATION_FAILED, + IN_DEREGISTRATION_OK, IN_DEREGISTRATION_FAILED, + IN_NO_SOCKET_CONNECTION, IN_SOCKET_CONNECTION_OK, + IN_NO_AVAILABLE_SERVICE, IN_SERVICE_AVAILABLE, + IN_TARGET_SOCKET_GRANTED, IN_TARGET_SOCKET_NOT_GRANTED } + + + +DEFINITIONS + //disjoint(rm_services) == !(a1,a2) . ( a1:dom(rm_services) & a2:dom(rm_services) & a1/=a2=>rm_services(a1)/\rm_services(a2)={} ); + SET_PREF_DEFAULT_SETSIZE == 2; + SET_PREF_MAX_OPERATIONS == 30; + scope_INTERCONNECTNODE == 2; + scope_SOCKET == 2; + scope_SERVICE == 2; + scope_RESOURCEMANAGER == 2; + scope_SID == 2 + +VARIABLES +/* these represent the objects */ + interconnectNodes, + sockets, + services, + resourceManagers, + sids, +/*and now the defintion of the classes and their internal and eternal datastructures*/ + rm_services, + rm_sids, + in_localServices, + in_sockets, + in_resourceManager, + soc_to, + soc_from, + svc_serviceID, + svc_sockets, + svc_ICNode, + svc_registered + + + + +INVARIANT + interconnectNodes <: INTERCONNECTNODE & + sockets <: SOCKET & + services <: SERVICE& + resourceManagers <: RESOURCEMANAGER & + sids <: SID & + + /*and now the invariants of the classes*/ + /*see page 99 of PUSSEE Book for explanations about the functions --> >+> etc */ + + rm_services : resourceManagers-->POW(services) & /* 0..1 -> 0..n */ + !(a1,a2) . ( a1:dom(rm_services) & a2:dom(rm_services) & a1/=a2=>rm_services(a1)/\rm_services(a2)={} ) & // was disjoint(rm_services) & + rm_sids : services>+>sids & + + + in_localServices : sids --> interconnectNodes & + in_sockets : sockets --> interconnectNodes & + in_resourceManager : interconnectNodes --> POW( resourceManagers ) & + + + + + + soc_to : sockets-->sids & + soc_from : sockets-->sids & + svc_serviceID : services+->sids & + svc_sockets : services-->POW(sockets) & + svc_ICNode : services--> interconnectNodes & + svc_registered : services-->BOOL & + + + /* invariants over the classes as a whole, ie: the triangles :) + !(ii, ss).( ( ii : interconnectNodes & ss : services & in_localServices(ii) = ss ) => in_sockets(ii) = svc_sockets(ss) ) & */ + /* only one resource manager in a system */ + /* at least for the moment, we might retrench this :-) in a more fault tolerant system */ + ( not(resourceManagers={}) => card(resourceManagers) = 1 ) + + + +INITIALISATION + interconnectNodes := {} || + sockets := {} || + services := {} || + resourceManagers := {} || + sids := {} || + /*and now the initialisations of the classes/objects */ + rm_services := {} || + rm_sids := {} || + in_localServices := {} || + in_sockets := {} || + in_resourceManager := {} || + soc_to := {} || + soc_from := {} || + svc_serviceID := {} || + svc_sockets := {} || + svc_ICNode := {} || + svc_registered := {} + + +/* constructors */ + +OPERATIONS + oid <-- constructor_interconnectNode(newic) = + SELECT + newic : INTERCONNECTNODE - interconnectNodes + THEN + interconnectNodes := interconnectNodes \/ { newic } || + in_resourceManager(newic) := {} || + oid := newic + END ; + + oid <-- constructor_resourceManager(newrm) = + PRE + resourceManagers = {} & + newrm : RESOURCEMANAGER - resourceManagers & + newrm /: dom(rm_services) + THEN + resourceManagers := resourceManagers \/ { newrm } || + rm_services(newrm) := {} || + oid := newrm + END ; + + oid <-- constructor_service(ii,newsvc) = + PRE + ii : interconnectNodes & + newsvc : SERVICE - services + THEN + services := services \/ { newsvc } || + svc_registered(newsvc) := FALSE || + svc_sockets(newsvc) := {} || + svc_ICNode(newsvc) := ii || + svc_serviceID := {} || + oid := newsvc + END ; + +/* generic constructor for socket Superclass*/ + oid <-- constructor_socket(ii,srcsid,targsid,newsoc) = + PRE + ii : interconnectNodes & + srcsid : sids & + targsid : sids & + newsoc : SOCKET - sockets + THEN + sockets := sockets \/ { newsoc } || + oid := newsoc || + in_sockets(newsoc) := ii || + soc_to(newsoc) := srcsid || + soc_from(newsoc) := targsid + END ; + + + + +/* end of constrctors */ + +/* Resource manager operations */ +rm_register(self,ss,ii) = + PRE + self : resourceManagers & + ss : services & /* this is the OBJECT */ + ii : interconnectNodes + THEN + skip + END ; + + rm_deregister(self,ss,ii) = + PRE + self : resourceManagers & + ss : services & + ii : interconnectNodes + THEN + skip + END ; + + sid,err<--rm_getSid(self,ss) = + PRE + self : resourceManagers & + ss : services & + ss:dom(rm_sids) THEN // ADDED + err := RM_SERVICE_FOUND || + sid := {rm_sids(ss)} // ORIGINALLY WD ERROR + END ; + sid,err<--rm_getSid_Not_Found(self,ss) = + PRE + self : resourceManagers & + ss : services + THEN + sid := SID-SID || + err := RM_SERVICE_NOT_FOUND + END ; + +/* interconnectNode */ + +in_announceResourceManager(self,rm) = + PRE + self : interconnectNodes & + rm : resourceManagers & + in_resourceManager(self) = {} + + THEN + in_resourceManager(self) := in_resourceManager(self) \/ { rm } + END ; + + +// Split for B2Program: + sid,err <-- in_register_success(self,ss,si) = + PRE + self : interconnectNodes & + ss : services & + si : SID - sids & + not(si : dom(in_localServices)) + THEN + sids := sids \/ { si } || + in_localServices := in_localServices \/ { si|->self } || + err := IN_REGISTRATION_OK || + sid := {si} + END; + + sid,err <-- in_register_failed(self,ss) = + PRE + self : interconnectNodes & + ss : services + THEN + sid := SID - SID || + err := IN_REGISTRATION_FAILED + END ; + + +// Split for B2Program: +soc,err <-- in_requestTargetSocket_Granted(self,ii,srcsoc,srcsid,targsid,newsoc) = +PRE + self : interconnectNodes & + ii : interconnectNodes & + self /= ii & + srcsoc : sockets & + in_sockets(srcsoc) = ii & + srcsid : sids & + targsid : sids & + newsoc : SOCKET - sockets + THEN + sockets := sockets \/ { newsoc } || + soc := { newsoc } || + err := IN_TARGET_SOCKET_GRANTED || + in_sockets := in_sockets \/ { newsoc |-> self } || + soc_to(newsoc) := srcsid || + soc_from(newsoc) := targsid +END ; +soc,err <-- in_requestTargetSocket_NotGranted(self,ii,srcsoc,srcsid,targsid) = +PRE + self : interconnectNodes & + ii : interconnectNodes & + self /= ii & + srcsoc : sockets & + in_sockets(srcsoc) = ii & + srcsid : sids & + targsid : sids +THEN + soc := SOCKET-SOCKET || + err := IN_TARGET_SOCKET_NOT_GRANTED + +END ; + + + + svc_register(self) = + PRE + self : services & + svc_registered(self) = FALSE + THEN + // CHOICE // not supported by B2Program + svc_registered(self) := TRUE + //OR + // svc_registered(self) := FALSE + // END + END + + + + +END diff --git a/benchmarks/model_checking_opreuse/ProB/prob_oneway8seq.mch b/benchmarks/model_checking_opreuse/ProB/prob_oneway8seq.mch index 1e38e37ca..028e1e2cf 100644 --- a/benchmarks/model_checking_opreuse/ProB/prob_oneway8seq.mch +++ b/benchmarks/model_checking_opreuse/ProB/prob_oneway8seq.mch @@ -1,5 +1,8 @@ /* https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax */ /* Model from https://mars-workshop.org/repository/020-CBTC.html */ +/* +F. Mazzanti and A. Ferrari. Ten diverse formal models for a cbtc automatic train supervision system. Electronic Proceedings in Theoretical Computer Science, 268:104–149, Mar. 2018. +*/ MACHINE prob_oneway8seq diff --git a/benchmarks/model_checking_opreuse/ProB/sort_m2_data1000_MC.mch b/benchmarks/model_checking_opreuse/ProB/sort_m2_data1000_MC.mch index 13d764409..b932db0c1 100644 --- a/benchmarks/model_checking_opreuse/ProB/sort_m2_data1000_MC.mch +++ b/benchmarks/model_checking_opreuse/ProB/sort_m2_data1000_MC.mch @@ -1,3 +1,7 @@ +/* +Original Model: +V. Rivera, N. Catano, T. Wahls, and C. Rueda. Code generation for Event-B. STTT, 19(1):31–52, 2017. +*/ MACHINE sort_m2_data1000_MC // a version where some assertions and invariants are simplified/removed // so that TLC4B can infer a function type for f and g diff --git a/benchmarks/model_checking_opreuse/TLC/LandingGear_R6.mch b/benchmarks/model_checking_opreuse/TLC/LandingGear_R6.mch index 72bd1819e..0c757ca06 100644 --- a/benchmarks/model_checking_opreuse/TLC/LandingGear_R6.mch +++ b/benchmarks/model_checking_opreuse/TLC/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/benchmarks/model_checking_opreuse/TLC/nota_v2.mch b/benchmarks/model_checking_opreuse/TLC/nota_v2.mch new file mode 100644 index 000000000..62b04c894 --- /dev/null +++ b/benchmarks/model_checking_opreuse/TLC/nota_v2.mch @@ -0,0 +1,300 @@ +MACHINE nota_v2 +// a simplified version of nota for B2Program + +/* these represent the classes */ +/* effectively these also include their addresses, which in an + OO context in their object ID. Note that also SERVICE also + includes the properties of those service objects, ie: the ID of + a service is more complicated than just an object id */ + + +SETS + INTERCONNECTNODE = {node1,node2}; + SOCKET = {socket1,socket2}; + SERVICE = {service1,service2}; + RESOURCEMANAGER = {resource1,resource2}; + SID = {SID1,SID2}; + +/* error codes */ + RM_ERROR_CODES = { RM_SERVICE_FOUND, RM_SERVICE_NOT_FOUND } ; + IN_ERROR_CODES = { IN_REGISTRATION_OK, IN_REGISTRATION_FAILED, + IN_DEREGISTRATION_OK, IN_DEREGISTRATION_FAILED, + IN_NO_SOCKET_CONNECTION, IN_SOCKET_CONNECTION_OK, + IN_NO_AVAILABLE_SERVICE, IN_SERVICE_AVAILABLE, + IN_TARGET_SOCKET_GRANTED, IN_TARGET_SOCKET_NOT_GRANTED } + + + +DEFINITIONS + //disjoint(rm_services) == !(a1,a2) . ( a1:dom(rm_services) & a2:dom(rm_services) & a1/=a2=>rm_services(a1)/\rm_services(a2)={} ); + SET_PREF_DEFAULT_SETSIZE == 2; + SET_PREF_MAX_OPERATIONS == 30; + scope_INTERCONNECTNODE == 2; + scope_SOCKET == 2; + scope_SERVICE == 2; + scope_RESOURCEMANAGER == 2; + scope_SID == 2 + +VARIABLES +/* these represent the objects */ + interconnectNodes, + sockets, + services, + resourceManagers, + sids, +/*and now the defintion of the classes and their internal and eternal datastructures*/ + rm_services, + rm_sids, + in_localServices, + in_sockets, + in_resourceManager, + soc_to, + soc_from, + svc_serviceID, + svc_sockets, + svc_ICNode, + svc_registered + + + + +INVARIANT + interconnectNodes <: INTERCONNECTNODE & + sockets <: SOCKET & + services <: SERVICE& + resourceManagers <: RESOURCEMANAGER & + sids <: SID & + + /*and now the invariants of the classes*/ + /*see page 99 of PUSSEE Book for explanations about the functions --> >+> etc */ + + rm_services : resourceManagers-->POW(services) & /* 0..1 -> 0..n */ + !(a1,a2) . ( a1:dom(rm_services) & a2:dom(rm_services) & a1/=a2=>rm_services(a1)/\rm_services(a2)={} ) & // was disjoint(rm_services) & + rm_sids : services>+>sids & + + + in_localServices : sids --> interconnectNodes & + in_sockets : sockets --> interconnectNodes & + in_resourceManager : interconnectNodes --> POW( resourceManagers ) & + + + + + + soc_to : sockets-->sids & + soc_from : sockets-->sids & + svc_serviceID : services+->sids & + svc_sockets : services-->POW(sockets) & + svc_ICNode : services--> interconnectNodes & + svc_registered : services-->BOOL & + + + /* invariants over the classes as a whole, ie: the triangles :) + !(ii, ss).( ( ii : interconnectNodes & ss : services & in_localServices(ii) = ss ) => in_sockets(ii) = svc_sockets(ss) ) & */ + /* only one resource manager in a system */ + /* at least for the moment, we might retrench this :-) in a more fault tolerant system */ + ( not(resourceManagers={}) => card(resourceManagers) = 1 ) + + + +INITIALISATION + interconnectNodes := {} || + sockets := {} || + services := {} || + resourceManagers := {} || + sids := {} || + /*and now the initialisations of the classes/objects */ + rm_services := {} || + rm_sids := {} || + in_localServices := {} || + in_sockets := {} || + in_resourceManager := {} || + soc_to := {} || + soc_from := {} || + svc_serviceID := {} || + svc_sockets := {} || + svc_ICNode := {} || + svc_registered := {} + + +/* constructors */ + +OPERATIONS + oid <-- constructor_interconnectNode(newic) = + SELECT + newic : INTERCONNECTNODE - interconnectNodes + THEN + interconnectNodes := interconnectNodes \/ { newic } || + in_resourceManager(newic) := {} || + oid := newic + END ; + + oid <-- constructor_resourceManager(newrm) = + PRE + resourceManagers = {} & + newrm : RESOURCEMANAGER - resourceManagers & + newrm /: dom(rm_services) + THEN + resourceManagers := resourceManagers \/ { newrm } || + rm_services(newrm) := {} || + oid := newrm + END ; + + oid <-- constructor_service(ii,newsvc) = + PRE + ii : interconnectNodes & + newsvc : SERVICE - services + THEN + services := services \/ { newsvc } || + svc_registered(newsvc) := FALSE || + svc_sockets(newsvc) := {} || + svc_ICNode(newsvc) := ii || + svc_serviceID := {} || + oid := newsvc + END ; + +/* generic constructor for socket Superclass*/ + oid <-- constructor_socket(ii,srcsid,targsid,newsoc) = + PRE + ii : interconnectNodes & + srcsid : sids & + targsid : sids & + newsoc : SOCKET - sockets + THEN + sockets := sockets \/ { newsoc } || + oid := newsoc || + in_sockets(newsoc) := ii || + soc_to(newsoc) := srcsid || + soc_from(newsoc) := targsid + END ; + + + + +/* end of constrctors */ + +/* Resource manager operations */ +rm_register(self,ss,ii) = + PRE + self : resourceManagers & + ss : services & /* this is the OBJECT */ + ii : interconnectNodes + THEN + skip + END ; + + rm_deregister(self,ss,ii) = + PRE + self : resourceManagers & + ss : services & + ii : interconnectNodes + THEN + skip + END ; + + sid,err<--rm_getSid(self,ss) = + PRE + self : resourceManagers & + ss : services & + ss:dom(rm_sids) THEN // ADDED + err := RM_SERVICE_FOUND || + sid := {rm_sids(ss)} // ORIGINALLY WD ERROR + END ; + sid,err<--rm_getSid_Not_Found(self,ss) = + PRE + self : resourceManagers & + ss : services + THEN + sid := SID-SID || + err := RM_SERVICE_NOT_FOUND + END ; + +/* interconnectNode */ + +in_announceResourceManager(self,rm) = + PRE + self : interconnectNodes & + rm : resourceManagers & + in_resourceManager(self) = {} + + THEN + in_resourceManager(self) := in_resourceManager(self) \/ { rm } + END ; + + +// Split for B2Program: + sid,err <-- in_register_success(self,ss,si) = + PRE + self : interconnectNodes & + ss : services & + si : SID - sids & + not(si : dom(in_localServices)) + THEN + sids := sids \/ { si } || + in_localServices := in_localServices \/ { si|->self } || + err := IN_REGISTRATION_OK || + sid := {si} + END; + + sid,err <-- in_register_failed(self,ss) = + PRE + self : interconnectNodes & + ss : services + THEN + sid := SID - SID || + err := IN_REGISTRATION_FAILED + END ; + + +// Split for B2Program: +soc,err <-- in_requestTargetSocket_Granted(self,ii,srcsoc,srcsid,targsid,newsoc) = +PRE + self : interconnectNodes & + ii : interconnectNodes & + self /= ii & + srcsoc : sockets & + in_sockets(srcsoc) = ii & + srcsid : sids & + targsid : sids & + newsoc : SOCKET - sockets + THEN + sockets := sockets \/ { newsoc } || + soc := { newsoc } || + err := IN_TARGET_SOCKET_GRANTED || + in_sockets := in_sockets \/ { newsoc |-> self } || + soc_to(newsoc) := srcsid || + soc_from(newsoc) := targsid +END ; +soc,err <-- in_requestTargetSocket_NotGranted(self,ii,srcsoc,srcsid,targsid) = +PRE + self : interconnectNodes & + ii : interconnectNodes & + self /= ii & + srcsoc : sockets & + in_sockets(srcsoc) = ii & + srcsid : sids & + targsid : sids +THEN + soc := SOCKET-SOCKET || + err := IN_TARGET_SOCKET_NOT_GRANTED + +END ; + + + + svc_register(self) = + PRE + self : services & + svc_registered(self) = FALSE + THEN + // CHOICE // not supported by B2Program + svc_registered(self) := TRUE + //OR + // svc_registered(self) := FALSE + // END + END + + + + +END diff --git a/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq.mch b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq.mch index 1e38e37ca..0de14d3d8 100644 --- a/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq.mch +++ b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq.mch @@ -1,6 +1,8 @@ /* https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax */ /* Model from https://mars-workshop.org/repository/020-CBTC.html */ - +/* +F. Mazzanti and A. Ferrari. Ten diverse formal models for a cbtc automatic train supervision system. Electronic Proceedings in Theoretical Computer Science, 268:104–149, Mar. 2018. +*/ MACHINE prob_oneway8seq DEFINITIONS diff --git a/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch index e178df054..cb4013c4b 100644 --- a/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch +++ b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch @@ -1,5 +1,8 @@ /* https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax */ - +/* Model from https://mars-workshop.org/repository/020-CBTC.html */ +/* +F. Mazzanti and A. Ferrari. Ten diverse formal models for a cbtc automatic train supervision system. Electronic Proceedings in Theoretical Computer Science, 268:104–149, Mar. 2018. +*/ MACHINE Oneway // addapted for TLC4B by Michael Leuschel // remove sequential composition in events -- GitLab