--transparent normal

M0 = < 1, 9,10,13,15,20,23>
M1 = < 3, 9,10,13,15,20,24>
M2 = < 5,27,11,13,16,20,25>
M3 = < 7,27,11,13,16,20,26>
M4 = <23,22,17,18,11, 9, 2>
M5 = <24,22,17,18,11, 9, 4>
M6 = <25,22,17,18,12,27, 6>
M7 = <26,22,17,18,12,27, 8>


  ------ region A: train constraints ------
A0 = < 0, 0, 0, 1, 0,-1, 0> -- G1
A1 = < 0, 0, 0, 1, 0,-1, 0> -- R1
A2 = < 0, 0, 1,-1, 0, 1, 0> -- Y1
A3 = < 0, 0, 1,-1, 0, 0, 0> -- B1
A4 = < 0, 1, 0, 0,-1, 0, 0> -- G2
A5 = < 0, 1, 0, 0,-1, 0, 0> -- R2
A6 = < 0, 0, 0,-1, 0, 0, 0> -- Y2
A7 = < 0, 1, 0,-1, 0, 0, 0> -- B2 
 ------------------------------------------

  ------- region B: train constraints ------
B0 = < 0, 0, 0, 1, 0,-1, 0> -- G1
B1 = < 0, 0, 0, 1, 0,-1, 0> -- R1
B2 = < 0, 0, 1,-1, 0, 0, 0> -- Y1
B3 = < 0, 0, 1,-1, 0, 1, 0> -- B1
B4 = < 0, 1, 0, 0,-1, 0, 0> -- G2
B5 = < 0, 1, 0, 0,-1, 0, 0> -- R2
B6 = < 0, 1, 0,-1, 0, 0, 0> -- Y2
B7 = < 0, 0, 0,-1, 0, 0, 0> -- B2
  ------------------------------------------
 
LA = 7
LB = 7

el(y,x) = if x==0 then head(y) else el(tail(y),x-1)

channel move:{1..27}.{1..27}.{ -1..1}.{ -1..1}
channel arrived


T0(p)=  ( p < 6 &  move!el(M0,p)!el(M0,p+1)!el(A0,p+1)!el(B0,p+1)
 			-> T0(p+1) )
        [] 
        ( p== 6 & arrived -> STOP )

T1(p)=  ( p < 6 & move!el(M1,p)!el(M1,p+1)!el(A1,p+1)!el(B1,p+1)
			-> T1(p+1) )
        [] 
        ( p== 6 & arrived -> STOP )

T2(p)=  ( p < 6 & move!el(M2,p)!el(M2,p+1)!el(A2,p+1)!el(B2,p+1)
			-> T2(p+1) )
        [] 
        ( p==6  & arrived -> STOP )

T3(p)=  ( p < 6 & move!el(M3,p)!el(M3,p+1)!el(A3,p+1)!el(B3,p+1)
			-> T3(p+1) )
        [] 
        ( p== 6 & arrived -> STOP )

T4(p)=  ( p < 6 & move!el(M4,p)!el(M4,p+1)!el(A4,p+1)!el(B4,p+1)
			-> T4(p+1) )
        [] 
        ( p==6 & arrived -> STOP )

T5(p)=  ( p < 6 & move!el(M5,p)!el(M5,p+1)!el(A5,p+1)!el(B5,p+1)
			-> T5(p+1))
        [] 
        ( p== 6 & arrived -> STOP )

T6(p)=  ( p < 6 & move!el(M6,p)!el(M6,p+1)!el(A6,p+1)!el(B6,p+1)
			-> T6(p+1) )
        [] 
        ( p== 6 & arrived -> STOP )

T7(p)=  ( p < 6 & move!el(M7,p)!el(M7,p+1)!el(A7,p+1)!el(B7,p+1)
			-> T7(p+1) )
        [] 
        ( p== 6 & arrived -> STOP )

FPLACE(x) =  
  (move?from:{z | z <-{1..27}, z != x}?to?a?b ->
     ((to == x & BPLACE(x))
       []
      (from !=x & to !=x & FPLACE(x))
     )
  )
   
BPLACE(x) =  
  ( move?from?to:{z | z <-{1..27}, z != x}?a?b ->
     ((from == x & FPLACE(x))
       []
       (from !=x & to !=x & BPLACE(x))
    )
  )


RA(n) = move?x?y!0?b -> RA(n) []
        n >0 & move?x?y!-1?b -> RA(n-1) []
        n<LA & move?x?y!1?b -> RA(n+1)

RB(n) = ( move?x?y?a!0 -> RB(n) )
        []
        ( n >0 & move?x?y?a!-1 -> RB(n-1) )
        []
        ( n<LB & move?x?y?a!1 -> RB(n+1) )
        

        
TRAINS =    T0(0) [|{|arrived|}|] 
           (T1(0) [|{|arrived|}|] 
           (T2(0) [|{|arrived|}|] 
           (T3(0) [|{|arrived|}|] 
           (T4(0) [|{|arrived|}|] 
           (T5(0) [|{|arrived|}|] 
           (T6(0) [|{|arrived|}|]
            T7(0) ))))))

SYS1 =   FPLACE(2) [|{|move|}|] 
       	(FPLACE(4) [|{|move|}|] 
       	(FPLACE(6) [|{|move|}|] 
       	(FPLACE(8) [|{|move|}|] 
       	(FPLACE(27) [|{|move|}|] 
       	(FPLACE(9) [|{|move|}|] 
       	(FPLACE(10) [|{|move|}|] 
       	(FPLACE(11) [|{|move|}|] 
       	(FPLACE(12) [|{|move|}|] 
       	(FPLACE(13) [|{|move|}|] 
       	(FPLACE(15) [|{|move|}|] 
       	(FPLACE(16) [|{|move|}|] 
       	(FPLACE(17) [|{|move|}|] 
       	(FPLACE(18) [|{|move|}|] 
       	(FPLACE(20) [|{|move|}|] 
       	(FPLACE(22) [|{|move|}|] 
       	(BPLACE(1) [|{|move|}|] 
       	(BPLACE(3) [|{|move|}|]
       	(BPLACE(5) [|{|move|}|]
       	(BPLACE(7) [|{|move|}|]
       	(BPLACE(23) [|{|move|}|]
       	(BPLACE(24) [|{|move|}|]
       	(BPLACE(25) [|{|move|}|]
       	(BPLACE(26) [|{|move|}|]
       	(RA(1)  [|{|move|}|] 
      	(RB(1)  [|{|move|}|] 
         TRAINS  )))) )))))))))))))))))))))
       		

-- hide unrelevant channels to improve compression
ASYS= SYS1\{|move|} 

SPEC = arrived -> STOP

assert SPEC [FD= ASYS


-------------------------------------------------------
--     verfication process :
-------------------------------------------------------
--  time ./FDR4.app/Contents/MacOS/refines fdr4_oneway8newsmall.txt
-- > 
-- > Result: Passed
-- >     Visited States: 1636546
-- >     Visited Transitions: 7134234
-- >     Visited Plys: 50
-- >     Estimated Total Storage: 268MB
-- > 
-- > real	0m41.722s
-- > user	1m41.775s
-- > sys	0m7.847s
-- > USED VIRTUAL MEMORY  650MB
-------------------------------------------------------

------------------------
--
--  when LA =8  the second assertion fails withthe counter-example:
--    ("--reveal-taus" for counter-examples)
--
------------------------
--https://www.cs.ox.ac.uk/projects/fdr/manual/optimising/overview.html#identifying-the-problem
------------------------
--- --refinement-storage-file-path /Users/mazzanti/Desktop/FDR4/swap/
--  to the command line version will cause FDR to store temporary data in the two directories. 
------------------------
-- assert P [T= Q :[partial order reduce [hybrid]]
--
--  compression is helpful for two verifications
--CSYS = normal(ASYS)