From 8f0ebc974dd98f63e91f6356de0be286b4ab8904 Mon Sep 17 00:00:00 2001
From: Fabian Vu <Fabian.Vu@hhu.de>
Date: Fri, 1 Nov 2024 11:34:24 +0100
Subject: [PATCH] Update a file for TLC benchmark
---
.../TLC/prob_oneway8seq_tlc.mch | 349 ++++++++++++++++++
1 file changed, 349 insertions(+)
create mode 100644 benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch
diff --git a/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch
new file mode 100644
index 000000000..e178df054
--- /dev/null
+++ b/benchmarks/model_checking_opreuse/TLC/prob_oneway8seq_tlc.mch
@@ -0,0 +1,349 @@
+/* https://www3.hhu.de/stups/prob/index.php/Summary_of_B_Syntax */
+
+MACHINE Oneway
+// addapted for TLC4B by Michael Leuschel
+// remove sequential composition in events
+// added constant values found by ProB to properties (not necessary if we use Setup by ProB option)
+// Note : ProB's AST cleanup will get rid of some of the sequential compositions
+// the B encoding could be made much more idiomatic and compact
+
+
+CONSTANTS
+ T0,T1,T2,T3,T4,T5,T6,T7,
+ A0,A1,A2,A3,A4,A5,A6,A7,
+ B0,B1,B2,B3,B4,B5,B6,B7,
+ LA,LB
+
+PROPERTIES
+
+ T0={(0|->1),(1|->9),(2|->10),(3|->13),(4|->15),(5|->20),(6|->23)} &
+ T1={(0|->3),(1|->9),(2|->10),(3|->13),(4|->15),(5|->20),(6|->24)} &
+ T2={(0|->5),(1|->27),(2|->11),(3|->13),(4|->16),(5|->20),(6|->25)} &
+ T3={(0|->7),(1|->27),(2|->11),(3|->13),(4|->16),(5|->20),(6|->26)} &
+ T4={(0|->23),(1|->22),(2|->17),(3|->18),(4|->11),(5|->9),(6|->2)} &
+ T5={(0|->24),(1|->22),(2|->17),(3|->18),(4|->11),(5|->9),(6|->4)} &
+ T6={(0|->25),(1|->22),(2|->17),(3|->18),(4|->12),(5|->27),(6|->6)} &
+ T7={(0|->26),(1|->22),(2|->17),(3|->18),(4|->12),(5|->27),(6|->8)} &
+ A0={(0|->0),(1|->0),(2|->0),(3|->1),(4|->0),(5|->-1),(6|->0)} &
+ A1={(0|->0),(1|->0),(2|->0),(3|->1),(4|->0),(5|->-1),(6|->0)} &
+ A2={(0|->0),(1|->0),(2|->1),(3|->-1),(4|->0),(5|->1),(6|->0)} &
+ A3={(0|->0),(1|->0),(2|->1),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+ A4={(0|->0),(1|->1),(2|->0),(3|->0),(4|->-1),(5|->0),(6|->0)} &
+ A5={(0|->0),(1|->1),(2|->0),(3|->0),(4|->-1),(5|->0),(6|->0)} &
+ A6={(0|->0),(1|->0),(2|->0),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+ A7={(0|->0),(1|->1),(2|->0),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+ B0={(0|->0),(1|->0),(2|->0),(3|->1),(4|->0),(5|->-1),(6|->0)} &
+ B1={(0|->0),(1|->0),(2|->0),(3|->1),(4|->0),(5|->-1),(6|->0)} &
+ B2={(0|->0),(1|->0),(2|->1),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+ B3={(0|->0),(1|->0),(2|->1),(3|->-1),(4|->0),(5|->1),(6|->0)} &
+ B4={(0|->0),(1|->1),(2|->0),(3|->0),(4|->-1),(5|->0),(6|->0)} &
+ B5={(0|->0),(1|->1),(2|->0),(3|->0),(4|->-1),(5|->0),(6|->0)} &
+ B6={(0|->0),(1|->1),(2|->0),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+ B7={(0|->0),(1|->0),(2|->0),(3|->-1),(4|->0),(5|->0),(6|->0)} &
+
+
+/*
+--------------------------------------------------------------
+T0: int[] := [ 1, 9,10,13,15,20,23]; -- G1
+T1: int[] := [ 3, 9,10,13,15,20,24]; -- R1
+T2: int[] := [ 5,27,11,13,16,20,25]; -- Y1
+T3: int[] := [ 7,27,11,13,16,20,26]; -- B1
+T4: int[] := [23,22,17,18,11, 9, 2]; -- G2
+T5: int[] := [24,22,17,18,11, 9, 4]; -- R2
+T6: int[] := [25,22,17,18,12,27, 6]; -- Y2
+T7: int[] := [26,22,17,18,12,27, 8]; -- B2
+----------------------------------------------------------------
+
+------ region A: train constraints ------
+A0: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- G1
+A1: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- R1
+A2: int[] := [ 0, 0, 1,-1, 0, 1, 0]; -- Y1
+A3: int[] := [ 0, 0, 1,-1, 0, 0, 0]; -- B1
+A4: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- G2
+A5: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- R2
+A6: int[] := [ 0, 0, 0,-1, 0, 0, 0]; -- Y2
+A7: int[] := [ 0, 1, 0,-1, 0, 0, 0]; -- B2
+------------------------------------------
+
+------- region B: train constraints ------
+B0: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- G1
+B1: int[] := [ 0, 0, 0, 1, 0,-1, 0]; -- R1
+B2: int[] := [ 0, 0, 1,-1, 0, 0, 0]; -- Y1
+B3: int[] := [ 0, 0, 1,-1, 0, 1, 0]; -- B1
+B4: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- G2
+B5: int[] := [ 0, 1, 0, 0,-1, 0, 0]; -- R2
+B6: int[] := [ 0, 1, 0,-1, 0, 0, 0]; -- Y2
+B7: int[] := [ 0, 0, 0,-1, 0, 0, 0]; -- B2
+------------------------------------------
+
+-------------------------------------------------------------
+RA: int :=1; -- initial value for region RA
+RB: int :=1; -- initial value for region RB
+LA: int :=7; -- limit value for region RA
+LB: int :=7; -- limit value for region RB
+-------------------------------------------------------------------
+*/
+
+ T0 : 0..6 --> 1..27 &
+ T1 : 0..6 --> 1..27 &
+ T2 : 0..6 --> 1..27 &
+ T3 : 0..6 --> 1..27 &
+ T4 : 0..6 --> 1..27 &
+ T5 : 0..6 --> 1..27 &
+ T6 : 0..6 --> 1..27 &
+ T7 : 0..6 --> 1..27 &
+
+ A0 : 0..6 --> -1..1 &
+ A1 : 0..6 --> -1..1 &
+ A2 : 0..6 --> -1..1 &
+ A3 : 0..6 --> -1..1 &
+ A4 : 0..6 --> -1..1 &
+ A5 : 0..6 --> -1..1 &
+ A6 : 0..6 --> -1..1 &
+ A7 : 0..6 --> -1..1 &
+
+ B0 : 0..6 --> -1..1 &
+ B1 : 0..6 --> -1..1 &
+ B2 : 0..6 --> -1..1 &
+ B3 : 0..6 --> -1..1 &
+ B4 : 0..6 --> -1..1 &
+ B5 : 0..6 --> -1..1 &
+ B6 : 0..6 --> -1..1 &
+ B7 : 0..6 --> -1..1 &
+
+ T0(0)= 1 & T0(1)= 9 & T0(2)=10 & T0(3)=13 & T0(4)=15 & T0(5)=20 & T0(6)=23 &
+ T1(0)= 3 & T1(1)= 9 & T1(2)=10 & T1(3)=13 & T1(4)=15 & T1(5)=20 & T1(6)=24 &
+ T2(0)= 5 & T2(1)=27 & T2(2)=11 & T2(3)=13 & T2(4)=16 & T2(5)=20 & T2(6)=25 &
+ T3(0)= 7 & T3(1)=27 & T3(2)=11 & T3(3)=13 & T3(4)=16 & T3(5)=20 & T3(6)=26 &
+ T4(0)=23 & T4(1)=22 & T4(2)=17 & T4(3)=18 & T4(4)=11 & T4(5)= 9 & T4(6)=2 &
+ T5(0)=24 & T5(1)=22 & T5(2)=17 & T5(3)=18 & T5(4)=11 & T5(5)= 9 & T5(6)=4 &
+ T6(0)=25 & T6(1)=22 & T6(2)=17 & T6(3)=18 & T6(4)=12 & T6(5)=27 & T6(6)=6 &
+ T7(0)=26 & T7(1)=22 & T7(2)=17 & T7(3)=18 & T7(4)=12 & T7(5)=27 & T7(6)=8 &
+
+ A0(0)=0 & A0(1)=0 & A0(2)=0 & A0(3)= 1 & A0(4)= 0 & A0(5)=-1 & A0( 6)=0 &
+ A1(0)=0 & A1(1)=0 & A1(2)=0 & A1(3)= 1 & A1(4)= 0 & A1(5)=-1 & A1( 6)=0 &
+ A2(0)=0 & A2(1)=0 & A2(2)=1 & A2(3)=-1 & A2(4)= 0 & A2(5)= 1 & A2( 6)=0 &
+ A3(0)=0 & A3(1)=0 & A3(2)=1 & A3(3)=-1 & A3(4)= 0 & A3(5)= 0 & A3( 6)=0 &
+ A4(0)=0 & A4(1)=1 & A4(2)=0 & A4(3)= 0 & A4(4)=-1 & A4(5)= 0 & A4( 6)=0 &
+ A5(0)=0 & A5(1)=1 & A5(2)=0 & A5(3)= 0 & A5(4)=-1 & A5(5)= 0 & A5( 6)=0 &
+ A6(0)=0 & A6(1)=0 & A6(2)=0 & A6(3)=-1 & A6(4)= 0 & A6(5)= 0 & A6( 6)=0 &
+ A7(0)=0 & A7(1)=1 & A7(2)=0 & A7(3)=-1 & A7(4)= 0 & A7(5)= 0 & A7( 6)=0 &
+
+ B0(0)=0 & B0(1)=0 & B0(2)=0 & B0(3)= 1 & B0(4)= 0 & B0(5)=-1 & B0( 6)=0 &
+ B1(0)=0 & B1(1)=0 & B1(2)=0 & B1(3)= 1 & B1(4)= 0 & B1(5)=-1 & B1( 6)=0 &
+ B2(0)=0 & B2(1)=0 & B2(2)=1 & B2(3)=-1 & B2(4)= 0 & B2(5)= 0 & B2( 6)=0 &
+ B3(0)=0 & B3(1)=0 & B3(2)=1 & B3(3)=-1 & B3(4)= 0 & B3(5)= 1 & B3( 6)=0 &
+ B4(0)=0 & B4(1)=1 & B4(2)=0 & B4(3)=-0 & B4(4)=-1 & B4(5)= 0 & B4( 6)=0 &
+ B5(0)=0 & B5(1)=1 & B5(2)=0 & B5(3)= 0 & B5(4)=-1 & B5(5)= 0 & B5( 6)=0 &
+ B6(0)=0 & B6(1)=1 & B6(2)=0 & B6(3)=-1 & B6(4)= 0 & B6(5)= 0 & B6( 6)=0 &
+ B7(0)=0 & B7(1)=0 & B7(2)=0 & B7(3)=-1 & B7(4)= 0 & B7(5)= 0 & B7( 6)=0 &
+
+ LA=7 & LB=7
+
+VARIABLES
+ P0,P1,P2,P3,P4,P5,P6,P7,RA,RB
+
+INVARIANT
+ P0:0..6 & P1:0..6 & P2:0..6 & P3:0..6 & P4:0..6 & P5:0..6 & P6:0..6 & P7:0..6 &
+ RA:0..8 & RB:0..8
+
+INITIALISATION
+ P0:=0 || P1:=0 || P2:=0 || P3:=0 || P4:=0 ||
+ P5:=0 || P6:=0 || P7:=0 || RA:=1 || RB:=1
+
+OPERATIONS
+ move0 =
+ PRE P0<6 &
+ T0(P0+1) /= T1(P1) & // next place of train0 not occupied by train1
+ T0(P0+1) /= T2(P2 )& // next place of train0 not occupied by train2
+ T0(P0+1) /= T3(P3 )&
+ T0(P0+1) /= T4(P4) &
+ T0(P0+1) /= T5(P5) &
+ T0(P0+1) /= T6(P6) &
+ T0(P0+1) /= T7(P7) & // next place of train0 not occupied by train7
+ RA + A0(P0+1) <= LA & // progress of train0 does not saturate RA
+ RB + B0(P0+1) <= LB // progress of train0 does not saturate RB
+ THEN
+ P0 := P0+1 ||
+ RA := RA + A0(P0+1) || // update occupancy of RA according to the step
+ RB := RB + B0(P0+1) // update occupancy of RB according to the step
+ END ;
+
+ move1 =
+ PRE P1<6 &
+ T1(P1+1) /= T0(P0) &
+ T1(P1+1) /= T2(P2) &
+ T1(P1+1) /= T3(P3) &
+ T1(P1+1) /= T4(P4) &
+ T1(P1+1) /= T5(P5) &
+ T1(P1+1) /= T6(P6) &
+ T1(P1+1) /= T7(P7) &
+ RA + A1(P1+1) <= LA &
+ RB + B1(P1+1) <= LB
+ THEN
+ P1 := P1+1 ||
+ RA := RA + A1(P1+1) ||
+ RB := RB + B1(P1+1)
+ END ;
+
+ move2 =
+ PRE P2<6 &
+ T2(P2+1) /= T0(P0) &
+ T2(P2+1) /= T1(P1) &
+ T2(P2+1) /= T3(P3) &
+ T2(P2+1) /= T4(P4) &
+ T2(P2+1) /= T5(P5) &
+ T2(P2+1) /= T6(P6) &
+ T2(P2+1) /= T7(P7) &
+ RA + A2(P2+1) <= LA &
+ RB + B2(P2+1) <= LB
+ THEN
+ P2 := P2+1 ||
+ RA := RA + A2(P2+1) ||
+ RB := RB + B2(P2+1)
+ END ;
+
+ move3 =
+ PRE P3<6 &
+ T3(P3+1) /= T0(P0) &
+ T3(P3+1) /= T1(P1) &
+ T3(P3+1) /= T2(P2) &
+ T3(P3+1) /= T4(P4) &
+ T3(P3+1) /= T5(P5) &
+ T3(P3+1) /= T6(P6) &
+ T3(P3+1) /= T7(P7) &
+ RA + A3(P3+1) <= LA &
+ RB + B3(P3+1) <= LB
+ THEN
+ P3 := P3+1 ||
+ RA := RA + A3(P3+1) ||
+ RB := RB + B3(P3+1)
+ END ;
+
+ move4 =
+ PRE P4<6 &
+ T4(P4+1) /= T0(P0) &
+ T4(P4+1) /= T1(P1) &
+ T4(P4+1) /= T2(P2) &
+ T4(P4+1) /= T3(P3) &
+ T4(P4+1) /= T5(P5) &
+ T4(P4+1) /= T6(P6) &
+ T4(P4+1) /= T7(P7) &
+ RA + A4(P4+1) <= LA &
+ RB + B4(P4+1) <= LB
+ THEN
+ P4 := P4+1 ||
+ RA := RA + A4(P4+1) ||
+ RB := RB + B4(P4+1)
+ END ;
+
+ move5 =
+ PRE P5<6 &
+ T5(P5+1) /= T0(P0) &
+ T5(P5+1) /= T1(P1) &
+ T5(P5+1) /= T2(P2) &
+ T5(P5+1) /= T3(P3) &
+ T5(P5+1) /= T4(P4) &
+ T5(P5+1) /= T6(P6) &
+ T5(P5+1) /= T7(P7) &
+ RA + A5(P5+1) <= LA &
+ RB + B5(P5+1) <= LB
+ THEN
+ P5 := P5+1 ||
+ RA := RA + A5(P5+1) ||
+ RB := RB + B5(P5+1)
+ END ;
+
+ move6 =
+ PRE P6<6 &
+ T6(P6+1) /= T0(P0) &
+ T6(P6+1) /= T1(P1) &
+ T6(P6+1) /= T2(P2) &
+ T6(P6+1) /= T3(P3) &
+ T6(P6+1) /= T4(P4) &
+ T6(P6+1) /= T5(P5) &
+ T6(P6+1) /= T7(P7) &
+ RA + A6(P6+1) <= LA &
+ RB + B6(P6+1) <= LB
+ THEN
+ P6 := P6+1 ||
+ RA := RA + A6(P6+1) ||
+ RB := RB + B6(P6+1)
+ END ;
+
+ move7 =
+ PRE P7<6 &
+ T7(P7+1) /= T0(P0) &
+ T7(P7+1) /= T1(P1) &
+ T7(P7+1) /= T2(P2) &
+ T7(P7+1) /= T3(P3) &
+ T7(P7+1) /= T4(P4) &
+ T7(P7+1) /= T5(P5) &
+ T7(P7+1) /= T6(P6) &
+ RA + A7(P7+1) <= LA &
+ RB + B7(P7+1) <= LB
+ THEN
+ P7 := P7+1 ||
+ RA := RA + A7(P7+1) ||
+ RB := RB + B7(P7+1)
+ END ;
+
+ arrived =
+ PRE
+ P0=6 & P1=6 & P2=6 & P3=6 & P4=6 & P5=6 & P6=6 & P7=6
+ THEN
+ skip
+ END
+END
+
+//--------------------
+// SEARCHING DEADLOCKS: 1_636_547 states, 7_134_235 trans. TIME 32 min VMEM 3 GB
+//-------------------
+
+/*
+> Model checking completed. No error has been found.
+> Estimates of the probability that TLC did not check all reachable states
+> because two distinct states had the same fingerprint:
+> calculated (optimistic): val = 4.9E-7
+> based on the actual fingerprints: val = 1.6E-9
+> The coverage statistics at 2024-06-26 15:28:42
+> End of statistics.
+> 7134234 states generated, 1636545 distinct states found, 0 states left on queue.
+> The depth of the complete state graph search is 48.
+> Finished. (2024-06-26 15:28:42)
+--------------------------------
+---------- Coverage statistics ----------
+move0: 944136
+move1: 944136
+move2: 900176
+move3: 900176
+move4: 840500
+move5: 840500
+move6: 882304
+move7: 882304
+arrived: 1
+---------- End of coverage statistics ----------
+Used Options
+| Number of workers: 2
+| Invariants check: false
+| Deadlock check: true
+| Assertion check: true
+| Find Goal check: false
+| LTL formulas check: false
+| Partial invariant evaluation: false
+| Lazy constants setup: true
+| Agressive well-definedness check: true
+| Prob constant setup: false
+| Symmetry reduction: false
+| MIN Int: 0
+| MAX Int: 1
+| Standard deferret set size: 3
+--------------------------------
+Parsing time: 452 ms
+Translation time: 126 ms
+Model checking time: 15 sec
+States analysed: 1636545
+Transitions fired: 7134234
+Result: NoError
+
+*/
--
GitLab