MACHINE C_m3_prob
CONCRETE_CONSTANTS
  T,
  a,
  b1,
  b2,
  tM,
  tm,
  v1,
  v2,
  vr,
  p,
  q,
  r
ABSTRACT_VARIABLES
  TT,
  new_now,
  temp,
  t2_c,
  now,
  t1_c,
  state,
  t1,
  t2,
  tp
/* PROMOTED OPERATIONS
  cool_rod1,
  cool_rod2,
  release_rod1,
  release_rod2,
  TIME_1,
  TIME_2,
  TIME_3 */
AXIOMS
    /* @C_c0:axm1 */ a : NAT
  & /* @C_c0:axm2 */ b1 : NAT
  & /* @C_c0:axm3 */ b2 : NAT
  & /* @C_c0:axm4 */ T : NAT
  & /* @C_c0:axm5 */ 2 * a + b1 >= T
  & /* @C_c0:axm6 */ 2 * a + b2 >= T
  & /* @C_c0:axm7 */ a < T
  & /* @C_c0:axm8 */ tm : NAT
  & /* @C_c0:axm9 */ tM : NAT
  & /* @C_c0:axm10 */ tM > tm
  & /* @C_c0:axm11 */ v1 : NAT
  & /* @C_c0:axm12 */ v2 : NAT
  & /* @C_c0:axm13 */ vr : NAT
  & /* @C_c0:axm14 */ v1 * b1 = tM - tm
  & /* @C_c0:axm15 */ v2 * b2 = tM - tm
  & /* @C_c0:axm16 */ vr * a = tM - tm
  & /* @C_c0:prob-ignore-axm17 */ !x,y,z.(
     x * y = x * z
     =>
     y = z
    ) /*@desc prob-ignore */
  & /* @C_c0_prob:prob1 */ a = 8
  & /* @C_c0_prob:prob2 */ b1 = 2
  & /* @C_c0_prob:prob3 */ b2 = 2
  & /* @C_c0_prob:prob4 */ T = 18
  & tM = 10
  & tm = 2
  & v1 = 4
  & v2 = 4
  & /* @C_c1:axm1 */ p > 0
  & /* @C_c1:axm2 */ q > 0
  & /* @C_c1:axm3 */ r > 0
INVARIANT
    /* @C_m3:inv2 */ new_now : NAT
  & /* @C_m3:inv3 */ (
     TT = FALSE
     =>
     new_now = now
    )
  & /* @C_m3:inv4 */ (
     (
      state = 1
      &
      TT = TRUE
     )
     =>
     new_now + b1 = now
    )
  & /* @C_m3:inv5 */ (
     (
      state = 2
      &
      TT = TRUE
     )
     =>
     new_now + b2 = now
    )
  & /* @C_m3:inv6 */ (
     (
      state = 0
      &
      TT = TRUE
     )
     =>
     new_now + a = now
    )
  & /* @C_m2:inv1 */ temp : NAT --> INT
  & /* @C_m2:inv2 */ tp = temp(now)
  & /* @C_m2:inv3 */ (
     (
      now >= a
      &
      state = 0
     )
     =>
     min({t|t >= now - a & temp(t) = tM}) = now
    )
  & /* @C_m2:inv4 */ (
     (
      now >= b1
      &
      state = 1
     )
     =>
     min({t|t >= now - b1 & temp(t) = tm}) = now
    )
  & /* @C_m2:inv5 */ (
     (
      now >= b2
      &
      state = 2
     )
     =>
     min({t|t >= now - b2 & temp(t) = tm}) = now
    )
  & /* @C_m1:inv1 */ now : NAT
  & /* @C_m1:inv3 */ t1_c : NAT --> INT /*@desc  */
  & /* @C_m1:inv7 */ t2_c : NAT --> INT /*@desc  */
  & /* @C_m1:inv5 */ t1 = t1_c(now) /*@desc  */
  & /* @C_m1:inv8 */ t2 = t2_c(now) /*@desc  */
  & /* @C_m0:inv1 */ t1 : NAT
  & /* @C_m0:inv2 */ t2 : NAT
  & /* @C_m0:inv3 */ state : {0,1,2}
  & /* @C_m0:inv4 */ (
     (
      state = 0
      &
      t1 >= T
     )
     =>
     t2 >= a
    )
  & /* @C_m0:inv5 */ (
     (
      state = 0
      &
      t2 >= T
     )
     =>
     t1 >= a
    )
  & /* @C_m0:inv6 */ (
     state = 1
     =>
     t2 >= a + b1
    )
  & /* @C_m0:inv7 */ (
     state = 2
     =>
     t1 >= a + b2
    )
  & /* @C_m0:inv8 */ (
     (
      state = 0
      &
      t1 >= T
     )
     =>
     (
      t1 >= 2 * a + b2
      &
      t2 = a
     )
    )
  & /* @C_m0:inv9 */ (
     (
      state = 0
      &
      t2 >= T
     )
     =>
     (
      t2 >= 2 * a + b1
      &
      t1 = a
     )
    )
  & /* @C_m0:inv10 */ (
     state = 0
     =>
     (
      t1 >= T
      or
      t2 >= T
     )
    )
  & /* @C_m0:inv11 */ tp : NAT
  & /* @C_m0:inv12 */ (
     state = 1
     =>
     tp = tm
    )
  & /* @C_m0:inv13 */ (
     state = 2
     =>
     tp = tm
    )
  & /* @C_m0:inv14 */ (
     state = 0
     =>
     tp = tM
    )
THEOREMS
     /* @C_m3:inv7 */ (
      (
       state = 0
       &
       TT = TRUE
      )
      =>
      min({t|t >= new_now & temp(t) = tM}) = new_now + a
     )
   ; /* @C_m3:inv8 */ (
      (
       state = 1
       &
       TT = TRUE
      )
      =>
      min({t|t >= new_now & temp(t) = tm}) = new_now + b1
     )
   ; /* @C_m3:inv9 */ (
      (
       state = 2
       &
       TT = TRUE
      )
      =>
      min({t|t >= new_now & temp(t) = tm}) = new_now + b2
     )
   ; /* @C_m1:thm */ (
      state = 0
      =>
      (
       t1_c(now) >= T
       or
       t2_c(now) >= T
      )
     )
INITIALISATION
    EVENT /* of machine C_m3_prob */
    BEGIN 
         t1_c := (/*@symbolic*/ %t.t : NAT|2 * a + b2)
      ||
         t2_c := (/*@symbolic*/ %t.t : NAT|a)
      ||
         state := 0
      ||
         temp := (/*@symbolic*/ %t.t : NAT|tM)
      ||
         TT := FALSE
      ||
         new_now := 0
    EXTENDS
      EVENT /* of machine C_m3 */
      REFINES 
        EVENT /* of machine C_m2 */
        BEGIN 
             now := 0
        REFINES 
          EVENT /* of machine C_m1 */
          BEGIN 
               tp := tM
          REFINES 
            EVENT /* of machine C_m0 */
            BEGIN 
                 t1 := 2 * a + b2
              ||
                 t2 := a
            END
          END
        END
    END
EVENTS
  cool_rod1 = 
    EVENT cool_rod1 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 0
      & /* @C_m3_prob:grd2 */ t1_c(new_now) >= T
      & /* @C_m3_prob:grd5 */ TT = FALSE
    THEOREMS 
        /* @C_m3_prob:grd3 */ temp(new_now) = tM
      & /* @C_m3_prob:grd4 */ b1 : NAT
    THEN 
         state := 1
      ||
         t2_c := t2_c <+ (/*@symbolic*/ %t.t >= new_now|t2_c(new_now) + (t - new_now))
      ||
         TT := TRUE
      ||
         t1_c := t1_c <+ (/*@symbolic*/ %t.t >= new_now|t1_c(new_now))
      ||
         temp := temp <+ (/*@symbolic*/ %t.t >= new_now|tM - v1 * (t - new_now))
    EXTENDS
      EVENT cool_rod1 = /* of machine C_m3 */
      REFINES 
        EVENT cool_rod1 = /* of machine C_m2 */
        WHEN 
            /* @C_m2:grd2 */ t1_c(now) >= T
        THEOREMS 
            /* @C_m2:grd3 */ temp(now) = tM
        THEN 
             t2_c := t2_c <+ (/*@symbolic*/ %t.t >= now|t2_c(now) + (t - now))
          ||
             now := now + b1
          ||
             t1_c := t1_c <+ (/*@symbolic*/ %t.t >= now|t1_c(now))
          ||
             temp := temp <+ (/*@symbolic*/ %t.t >= now|tM - v1 * (t - now))
        REFINES 
          EVENT cool_rod1 = /* of machine C_m1 */
          THEOREMS 
              /* @C_m1:grd3 */ tp = tM
          BEGIN 
               tp := tm
          REFINES 
            EVENT cool_rod1 = /* of machine C_m0 */
            WHEN 
                /* @C_m0:grd2 */ t1 >= T
            THEN 
                 t2 := t2 + b1
            END
          END
        END
    END;
  
  cool_rod2 = 
    EVENT cool_rod2 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 0
      & /* @C_m3_prob:grd2 */ t2_c(new_now) >= T
      & /* @C_m3_prob:grd5 */ TT = FALSE
    THEOREMS 
        /* @C_m3_prob:grd3 */ temp(new_now) = tM
      & /* @C_m3_prob:grd4 */ b2 : NAT
    THEN 
         state := 2
      ||
         t1_c := t1_c <+ (/*@symbolic*/ %t.t >= new_now|t1_c(new_now) + (t - new_now))
      ||
         TT := TRUE
      ||
         t2_c := t2_c <+ (/*@symbolic*/ %t.t >= new_now|t2_c(new_now))
      ||
         temp := temp <+ (/*@symbolic*/ %t.t >= new_now|tM - v2 * (t - new_now))
    EXTENDS
      EVENT cool_rod2 = /* of machine C_m3 */
      REFINES 
        EVENT cool_rod2 = /* of machine C_m2 */
        WHEN 
            /* @C_m2:grd2 */ t2_c(now) >= T
        THEOREMS 
            /* @C_m2:grd3 */ temp(now) = tM
        THEN 
             t1_c := t1_c <+ (/*@symbolic*/ %t.t >= now|t1_c(now) + (t - now))
          ||
             now := now + b2
          ||
             t2_c := t2_c <+ (/*@symbolic*/ %t.t >= now|t2_c(now))
          ||
             temp := temp <+ (/*@symbolic*/ %t.t >= now|tM - v2 * (t - now))
        REFINES 
          EVENT cool_rod2 = /* of machine C_m1 */
          THEOREMS 
              /* @C_m1:grd3 */ tp = tM
          BEGIN 
               tp := tm
          REFINES 
            EVENT cool_rod2 = /* of machine C_m0 */
            WHEN 
                /* @C_m0:grd2 */ t2 >= T
            THEN 
                 t1 := t1 + b2
            END
          END
        END
    END;
  
  release_rod1 = 
    EVENT release_rod1 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 1
      & /* @C_m3_prob:grd4 */ TT = FALSE
    THEOREMS 
        /* @C_m3_prob:grd2 */ temp(new_now) = tm
      & /* @C_m3_prob:grd3 */ a : NAT
    THEN 
         state := 0
      ||
         t1_c := t1_c <+ (/*@symbolic*/ %t.t >= new_now|t - new_now)
      ||
         t2_c := t2_c <+ (/*@symbolic*/ %t.t >= new_now|t2_c(new_now) + (t - new_now))
      ||
         TT := TRUE
      ||
         temp := temp <+ (/*@symbolic*/ %t.t >= new_now|tm + vr * (t - new_now))
    EXTENDS
      EVENT release_rod1 = /* of machine C_m3 */
      REFINES 
        EVENT release_rod1 = /* of machine C_m2 */
        THEOREMS 
            /* @C_m2:grd2 */ temp(now) = tm
        BEGIN 
             t1_c := t1_c <+ (/*@symbolic*/ %t.t >= now|t - now)
          ||
             t2_c := t2_c <+ (/*@symbolic*/ %t.t >= now|t2_c(now) + (t - now))
          ||
             now := now + a
          ||
             temp := temp <+ (/*@symbolic*/ %t.t >= now|tm + vr * (t - now))
        REFINES 
          EVENT release_rod1 = /* of machine C_m1 */
          THEOREMS 
              /* @C_m1:grd2 */ tp = tm
          BEGIN 
               tp := tM
          REFINES 
            EVENT release_rod1 = /* of machine C_m0 */
            BEGIN 
                 t1 := a
              ||
                 t2 := t2 + a
            END
          END
        END
    END;
  
  release_rod2 = 
    EVENT release_rod2 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 2
      & /* @C_m3_prob:grd4 */ TT = FALSE
    THEOREMS 
        /* @C_m3_prob:grd2 */ temp(new_now) = tm
      & /* @C_m3_prob:grd3 */ a : NAT
    THEN 
         state := 0
      ||
         t1_c := t1_c <+ (/*@symbolic*/ %t.t >= new_now|t1_c(new_now) + (t - new_now))
      ||
         t2_c := t2_c <+ (/*@symbolic*/ %t.t >= new_now|t - new_now)
      ||
         TT := TRUE
      ||
         temp := temp <+ (/*@symbolic*/ %t.t >= new_now|tm + vr * (t - new_now))
    EXTENDS
      EVENT release_rod2 = /* of machine C_m3 */
      REFINES 
        EVENT release_rod2 = /* of machine C_m2 */
        THEOREMS 
            /* @C_m2:grd2 */ temp(now) = tm
        BEGIN 
             t1_c := t1_c <+ (/*@symbolic*/ %t.t >= now|t1_c(now) + (t - now))
          ||
             t2_c := t2_c <+ (/*@symbolic*/ %t.t >= now|t - now)
          ||
             now := now + a
          ||
             temp := temp <+ (/*@symbolic*/ %t.t >= now|tm + vr * (t - now))
        REFINES 
          EVENT release_rod2 = /* of machine C_m1 */
          THEOREMS 
              /* @C_m1:grd2 */ tp = tm
          BEGIN 
               tp := tM
          REFINES 
            EVENT release_rod2 = /* of machine C_m0 */
            BEGIN 
                 t1 := t1 + a
              ||
                 t2 := a
            END
          END
        END
    END;
  
  TIME_1 = 
    EVENT TIME_1 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 1
      & /* @C_m3_prob:grd2 */ TT = TRUE
    THEN 
         new_now := new_now + b1
      ||
         TT := FALSE
    EXTENDS
      EVENT TIME_1 = /* of machine C_m3 */
    END;
  
  TIME_2 = 
    EVENT TIME_2 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 2
      & /* @C_m3_prob:grd2 */ TT = TRUE
    THEN 
         new_now := new_now + b2
      ||
         TT := FALSE
    EXTENDS
      EVENT TIME_2 = /* of machine C_m3 */
    END;
  
  TIME_3 = 
    EVENT TIME_3 = /* of machine C_m3_prob */
    WHEN 
        /* @C_m3_prob:grd1 */ state = 0
      & /* @C_m3_prob:grd2 */ TT = TRUE
    THEN 
         new_now := new_now + a
      ||
         TT := FALSE
    EXTENDS
      EVENT TIME_3 = /* of machine C_m3 */
    END
END