pta

formula fk1S1 = (sF1=1);
formula fk2S1 = (sS1=3);
formula fk1S2 = (sF2=1);
formula fk2S2 = (sS2=3);
formula fk3S2 = (sF1=1);
formula fk4S2 = (sS2=5);
formula fk1S3 = (sF2=1);
formula fk2S3 = (sS3=3);
formula fk3S3 = (sB=1) | (sB=5);
formula fk4S3 = (sS3=5);
formula fk1F2 = (sB=1) | (sB=3);
formula fk2F2 = (sF2=4);
formula flock1 = (sF1=4) | (sB=8) | (sR=1);
formula flock2 = (sM=1);
formula funlock1 = (sF1=7) | (sB=11) | (sR=4);
formula funlock2 = (sM=3);



module mS1
    xS1 : clock;
    sS1 : [0..3] init 0;
    
    invariant
        (sS1=0 => xS1 <= 75) &
        (sS1=1 => xS1 <= 100) &
        (sS1=2 => xS1 <= 0) 
    endinvariant

    [] sS1=0 & xS1 >= 50 -> (sS1'=1) & (xS1'=0);
    [] sS1=1 & xS1 >= 75 -> (sS1'=2) & (xS1'=0);
    [k1S1] sS1=2 -> (sS1'=1) & (xS1'=0);
    [] sS1=2 & !fk1S1 -> (sS1'=3);
    [k2S1] sS1=3 -> (sS1'=1) & (xS1'=0);
endmodule

module mS2
    xS2 : clock;
    sS2 : [0..5] init 0;
    
    invariant
        (sS2=0 => xS2 <= 300) &
        (sS2=1 => xS2 <= 400) &
        (sS2=2 => xS2 <= 0) &
        (sS2=4 => xS2 <= 0)
    endinvariant

    [] sS2=0 & xS2 >= 200 -> (sS2'=1) & (xS2'=0);
    [] sS2=1 & xS2 >= 350 -> (sS2'=2) & (xS2'=0);
    [k1S2] sS2=2 -> (sS2'=4) & (xS2'=0);
    [] sS2=2 & !fk1S2 -> (sS2'=3);
    [k2S2] sS2=3 -> (sS2'=4) & (xS2'=0);
    [k3S2] sS2=4 -> (sS2'=1) & (xS2'=0);
    [] sS2=4 & !fk3S2 -> (sS2'=5);
    [k4S2] sS2=5 -> (sS2'=1) & (xS2'=0);
endmodule

module mS3
    xS3 : clock;
    sS3 : [0..5] init 0;
    
    invariant
        (sS3=0 => xS3 <= 300) &
        (sS3=1 => xS3 <= 400) &
        (sS3=2 => xS3 <= 0) &
        (sS3=4 => xS3 <= 0)
    endinvariant

    [] sS3=0 & xS3 >= 200 -> (sS3'=1) & (xS3'=0);
    [] sS3=1 & xS3 >= 350 -> (sS3'=2) & (xS3'=0);
    [k1S3] sS3=2 -> (sS3'=4) & (xS3'=0);
    [] sS3=2 & !fk1S3 -> (sS3'=3);
    [k2S3] sS3=3 -> (sS3'=4) & (xS3'=0);
    [k3S3] sS3=4 -> (sS3'=1) & (xS3'=0);
    [] sS3=4 & !fk3S3 -> (sS3'=5);
    [k4S3] sS3=5 -> (sS3'=1) & (xS3'=0);
endmodule

module mF1
    xF1 : clock;
    sF1 : [0..7] init 0;

    invariant 
        (sF1=0 => xF1<=0) &
        (sF1=2 => xF1<=75) &
        (sF1=3 => xF1<=0) &
        (sF1=5 => xF1<=50) &
        (sF1=6 => xF1<=0) 
    endinvariant

    [k4S2] sF1=0 -> (sF1'=2) & (xF1'=0);
    [k2S1] sF1=0 -> (sF1'=2) & (xF1'=0);
    [] sF1=0 & !fk4S2 & !fk2S1 -> (sF1'=1);
    [k3S2] sF1=1 -> (sF1'=2) & (xF1'=0);
    [k1S1] sF1=1 -> (sF1'=2) & (xF1'=0);
    [] sF1=2 & xF1 >= 50 -> (sF1'=3) & (xF1'=0);
    [] sF1=3 & !flock2 -> (sF1'=4);
    [lock2F1] sF1=3 -> (sF1'=5) & (xF1'=0);
    [lock1F1] sF1=4 -> (sF1'=5) & (xF1'=0);
    [] sF1=5 & xF1 >= 25 -> (sF1'=6) & (xF1'=0);
    [] sF1=6 & !funlock2 -> (sF1'=7);
    [unlock2F1] sF1=6 -> (sF1'=0) & (xF1'=0);
    [unlock1F1] sF1=7 -> (sF1'=0) & (xF1'=0);
    
endmodule

module mF2
    xF2 : clock;
    sF2 : [0..4] init 0;

    invariant 
        (sF2=0 => xF2<=0) &
        (sF2=2 => xF2<=100) &
        (sF2=3 => xF2<=0)
    endinvariant

    [k2S3] sF2=0 -> (sF2'=2) & (xF2'=0);
    [k2S2] sF2=0 -> (sF2'=2) & (xF2'=0);
    [] sF2=0 & !fk2S3 & !fk2S2 -> (sF2'=1);
    [k1S3] sF2=1 -> (sF2'=2) & (xF2'=0);
    [k1S2] sF2=1 -> (sF2'=2) & (xF2'=0);
    [] sF2=2 & xF2 >= 75 -> (sF2'=3) & (xF2'=0);
    [] sF2=3 & !fk1F2 -> (sF2'=4);
    [k1F2] sF2=3 -> (sF2'=0) & (xF2'=0);
    [k2F2] sF2=4 -> (sF2'=0) & (xF2'=0);
    
endmodule

module mB
    xB : clock;
    sB : [0..11] init 0;

    invariant 
        (sB=0 => xB<=0) &
        (sB=2 => xB<=0) &
        (sB=4 => xB<=0) &
        (sB=6 => xB<=50) &
        (sB=7 => xB<=0) &
        (sB=9 => xB<=50) &
        (sB=10 => xB<=0) 
    endinvariant

    [k4S3] sB=0 -> (sB'=2) & (xB'=0);
    [k2F2] sB=0 -> (sB'=4) & (xB'=0);
    [] sB=0 & !fk4S3 & !fk2F2 -> (sB'=1);
    [k3S3] sB=1 -> (sB'=2) & (xB'=0);
    [k1F2] sB=1 -> (sB'=4) & (xB'=0);
    [k2F2] sB=2 -> (sB'=6) & (xB'=0);
    [] sB=2 & !fk2F2 -> (sB'=3);
    [k1F2] sB=3 -> (sB'=6) & (xB'=0);
    [k4S3] sB=4 -> (sB'=6) & (xB'=0);
    [] sB=4 & !fk4S3 -> (sB'=5);
    [k3S3] sB=5 -> (sB'=6) & (xB'=0);
    [] sB=6 & xB >= 25 -> (sB'=7) & (xB'=0);
    [lock2B] sB=7 -> (sB'=9) & (xB'=0);
    [] sB=7 & !flock2 -> (sB'=8);
    [lock1B] sB=8 -> (sB'=9) & (xB'=0);
    [] sB=9 & xB >= 25 -> (sB'=10) & (xB'=0);
    [unlock2B] sB=10 -> (sB'=0) & (xB'=0);
    [] sB=10 & !funlock2 -> (sB'=11);
    [unlock1B] sB=11 -> (sB'=0) & (xB'=0);
    
endmodule

module mM
    xM : clock;
    sM : [0..3] init 1;

    invariant 
        (sM=0 => xM<=0) &
        (sM=2 => xM<=0)
    endinvariant

    [] sM=0 & !flock1-> (sM'=1);
    [lock1B] sM=0 -> (sM'=2) & (xM'=0);
    [lock1F1] sM=0 -> (sM'=2) & (xM'=0);
    [lock1R] sM=0 -> (sM'=2) & (xM'=0);
    [lock2B] sM=1 -> (sM'=2) & (xM'=0);
    [lock2F1] sM=1 -> (sM'=2) & (xM'=0);
    [lock2R] sM=1 -> (sM'=2) & (xM'=0);
    [] sM=2 & !funlock1 -> (sM'=3);
    [unlock1B] sM=2 -> (sM'=0) & (xM'=0);
    [unlock1F1] sM=2 -> (sM'=0) & (xM'=0);
    [unlock1R] sM=2 -> (sM'=0) & (xM'=0);
    [unlock2B] sM=3 -> (sM'=0) & (xM'=0);
    [unlock2F1] sM=3 -> (sM'=0) & (xM'=0);
    [unlock2R] sM=3 -> (sM'=0) & (xM'=0);

endmodule

module mR
    xR : clock;
    sR : [0..5] init 0;

    invariant 
         (sR=0 => xR<=0) &
         (sR=2 => xR<=50) &
         (sR=3 => xR<=0) &
         (sR=5 => xR<=75)
    endinvariant

    [lock2R] sR=0 -> (sR'=2) & (xR'=0);
    [] sR=0 & !flock2 -> (sR'=1);
    [lock1R] sR=1 -> (sR'=2) & (xR'=0);
    [] sR=2 & xR >= 25 -> (sR'=3) & (xR'=0);
    [unlock2R] sR=3 -> (sR'=5) & (xR'=0);
    [] sR=3 & !funlock2 -> (sR'=4);
    [unlock1R] sR=4 -> (sR'=5) & (xR'=0);
    [] sR=5 & xR >= 50 -> (sR'=0) & (xR'=0);

endmodule