The DisCo Home Page

PVS Theory "rides_assertions"

rides_assertions: THEORY
  BEGIN
  
  IMPORTING rides
  
  customer_unique_reference: bool =
    FORALL (obj1, obj2: customer): ref(obj1) = ref(obj2) IMPLIES obj1 = obj2
  
  cab_unique_reference: bool =
    FORALL (obj1, obj2: cab): ref(obj1) = ref(obj2) IMPLIES obj1 = obj2
  
  taxi_stand_unique_reference: bool =
    FORALL (obj1, obj2: taxi_stand): ref(obj1) = ref(obj2) IMPLIES obj1 = obj2
  
  idle_outside_strengthening_body((c: customer), (other: state)): bool =
    NOT(((waiting_for_cab?(state1(c)(other)))
             AND NOT((outside?(state2(c)(other))))))
        AND
      NOT(((idle?(state1(c)(other))) AND NOT((outside?(state2(c)(other))))))
  
  idle_outside_strengthening((other: state)): bool =
    (FORALL (c: customer): idle_outside_strengthening_body(c, other))
  
  idle_outside_body((c: customer), (other: state)): bool =
    (idle?(state1(c)(other))) IMPLIES (outside?(state2(c)(other)))
  
  idle_outside((other: state)): bool =
    (FORALL (c: customer): idle_outside_body(c, other))
  
  inside_engaged_strengthening_body((cb: cab),
                                    (c2: customer), (c1: customer),
                                    (other: state)):
      bool =
    NOT(((in_cab?(state2(c1)(other)))
             AND
           ((in_cab_which(c1)(other) = ref(cb))
                AND
              NOT(((on_the_road_engaged?(state3(cb)(other)))
                       AND (on_the_road?(state4(cb)(other))))))))
        AND
      NOT(((in_cab?(state2(c1)(other)))
               AND
             ((in_cab_which(c1)(other) = ref(cb))
                  AND
                ((in_cab?(state2(c2)(other)))
                     AND
                   ((in_cab_which(c2)(other) = ref(cb))
                        AND NOT((ref(c1) = ref(c2))))))))
  
  inside_engaged_strengthening((other: state)): bool =
    (FORALL (c1: customer):
       (FORALL (c2: customer):
          (FORALL (cb: cab):
             inside_engaged_strengthening_body(cb, c2, c1, other))))
  
  inside_engaged_body((cb: cab), (c: customer), (other: state)): bool =
    ((in_cab?(state2(c)(other))) AND (in_cab_which(c)(other) = ref(cb)))
        IMPLIES
      ((on_the_road_engaged?(state3(cb)(other)))
           AND (on_the_road?(state4(cb)(other))))
  
  inside_engaged((other: state)): bool =
    (FORALL (c: customer):
       (FORALL (cb: cab): inside_engaged_body(cb, c, other)))
  
  ASSUMPTIONS: bool =
    TRUE
        AND customer_unique_reference
          AND cab_unique_reference AND taxi_stand_unique_reference
  
  INIT((other: state)): bool =
    idle_outside_strengthening(other)
        AND idle_outside(other)
          AND inside_engaged_strengthening(other) AND inside_engaged(other)
  
  ACTIONS((s, sp: state)): bool =
    start_ride(s, sp)
        OR start_waiting(s, sp)
          OR end_ride(s, sp)
            OR enter_stand(s, sp)
              OR get_service(s, sp) OR stop_waiting(s, sp) OR exit_stand(s, sp)
  
  start_ride_preserves_idle_outside_strengthening: LEMMA
        preserves(start_ride, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  start_waiting_preserves_idle_outside_strengthening: LEMMA
        preserves(start_waiting, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  end_ride_preserves_idle_outside_strengthening: LEMMA
        preserves(end_ride, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  enter_stand_preserves_idle_outside_strengthening: LEMMA
        preserves(enter_stand, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  get_service_preserves_idle_outside_strengthening: LEMMA
        preserves(get_service, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  stop_waiting_preserves_idle_outside_strengthening: LEMMA
        preserves(stop_waiting, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  exit_stand_preserves_idle_outside_strengthening: LEMMA
        preserves(exit_stand, idle_outside_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  idle_outside_strengthening_is_invariant: THEOREM
        invariant(idle_outside_strengthening, ASSUMPTIONS, INIT, ACTIONS)
  
  start_ride_preserves_idle_outside: LEMMA
        preserves(start_ride, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  start_waiting_preserves_idle_outside: LEMMA
        preserves(start_waiting, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  end_ride_preserves_idle_outside: LEMMA
        preserves(end_ride, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  enter_stand_preserves_idle_outside: LEMMA
        preserves(enter_stand, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  get_service_preserves_idle_outside: LEMMA
        preserves(get_service, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  stop_waiting_preserves_idle_outside: LEMMA
        preserves(stop_waiting, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  exit_stand_preserves_idle_outside: LEMMA
        preserves(exit_stand, idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  idle_outside_is_invariant: THEOREM
        invariant(idle_outside, ASSUMPTIONS, INIT, ACTIONS)
  
  start_ride_preserves_inside_engaged_strengthening: LEMMA
        preserves(start_ride, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  start_waiting_preserves_inside_engaged_strengthening: LEMMA
        preserves(start_waiting, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  end_ride_preserves_inside_engaged_strengthening: LEMMA
        preserves(end_ride, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  enter_stand_preserves_inside_engaged_strengthening: LEMMA
        preserves(enter_stand, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  get_service_preserves_inside_engaged_strengthening: LEMMA
        preserves(get_service, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  stop_waiting_preserves_inside_engaged_strengthening: LEMMA
        preserves(stop_waiting, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  exit_stand_preserves_inside_engaged_strengthening: LEMMA
        preserves(exit_stand, inside_engaged_strengthening,
                  ASSUMPTIONS, INIT, ACTIONS)
  
  inside_engaged_strengthening_is_invariant: THEOREM
        invariant(inside_engaged_strengthening, ASSUMPTIONS, INIT, ACTIONS)
  
  start_ride_preserves_inside_engaged: LEMMA
        preserves(start_ride, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  start_waiting_preserves_inside_engaged: LEMMA
        preserves(start_waiting, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  end_ride_preserves_inside_engaged: LEMMA
        preserves(end_ride, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  enter_stand_preserves_inside_engaged: LEMMA
        preserves(enter_stand, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  get_service_preserves_inside_engaged: LEMMA
        preserves(get_service, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  stop_waiting_preserves_inside_engaged: LEMMA
        preserves(stop_waiting, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  exit_stand_preserves_inside_engaged: LEMMA
        preserves(exit_stand, inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  inside_engaged_is_invariant: THEOREM
        invariant(inside_engaged, ASSUMPTIONS, INIT, ACTIONS)
  
  END rides_assertions