DisCo Logo  

The DisCo Home Page

Main Page
Disco in a Nutshell
Formal Issues
Publications
Bugreporting
Members
Links

PVS Theory "rides"

This PVS theory describes the classes and actions in the taxi cabs example. Theorems corresponding to actions are given in theory rides_assertions. 
rides: THEORY
BEGIN

discolib: LIBRARY = "/home/korppi-a/pk/vaikkari/pdp/pvs"

IMPORTING discolib@mod

IMPORTING discolib@discoev

state1_type: TYPE = {idle, waiting_for_cab, being_served}

state2_type: TYPE = {outside, in_cab}

customer:
TYPE FROM
[# state1: [state -> state1_type],
   waiting_for_cab_where: [state -> objid],
   state2: [state -> state2_type],
   in_cab_which: [state -> objid],
   ref: objid #]

state4_type: TYPE = {on_the_road, at_stand}

state3_type: TYPE = {on_the_road_free, on_the_road_engaged}

cab:
TYPE FROM
[# state4: [state -> state4_type],
   state3: [state -> state3_type],
   at_stand_where: [state -> objid],
   ref: objid #]

taxi_stand: TYPE FROM [# ref: objid #]

start_ride_guard((cb: cab), (c: customer), (other: state)): bool =
(at_stand?(state4(cb)(other)))
AND
((waiting_for_cab?(state1(c)(other)))
 AND
 (((at_stand_where(cb)(other)) = waiting_for_cab_where(c)(other))
  AND
  ((outside?(state2(c)(other)))
   AND
   ((at_stand?(state4(cb)(other))) AND (waiting_for_cab?(state1(c)(other)))))))

start_ride((unprimed, primed: state)): bool =
(EXISTS (cb: cab, c: customer):
 (start_ride_guard(cb, c, unprimed))
 AND
 (((on_the_road?(state4(cb)(primed)))
   AND
   ((being_served?(state1(c)(primed)))
    AND
    ((in_cab?(state2(c)(primed)))
     AND
     ((in_cab_which(c)(primed) = (ref(cb)))
      AND
      ((on_the_road?(state4(cb)(primed)))
       AND (on_the_road_engaged?(state3(cb)(primed))))))))
  AND
  (((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES (state1(other)(primed) = (state1(other)(unprimed)))))
   AND
   (((FORALL (other: customer):
      ((other) /= (c))
      IMPLIES
      (waiting_for_cab_where(other)(primed)
       = (waiting_for_cab_where(other)(unprimed)))))
    AND
    (((FORALL (other: customer):
       ((other) /= (c))
       IMPLIES (state2(other)(primed) = (state2(other)(unprimed)))))
     AND
     (((FORALL (other: customer):
        ((other) /= (c))
        IMPLIES
        (in_cab_which(other)(primed) = (in_cab_which(other)(unprimed)))))
      AND
      (((FORALL (other: cab):
         ((other) /= (cb))
         IMPLIES (state4(other)(primed) = (state4(other)(unprimed)))))
       AND
       (((FORALL (other: cab):
          ((other) /= (cb))
          IMPLIES (state3(other)(primed) = (state3(other)(unprimed)))))
        AND
        ((FORALL (other: cab):
          ((other) /= (cb))
          IMPLIES
          (at_stand_where(other)(primed)
           = (at_stand_where(other)(unprimed)))))))))))))
AND TRUE

start_waiting_guard((c: customer), (s: taxi_stand), (other: state)):
bool = idle?(state1(c)(other))

start_waiting((unprimed, primed: state)): bool =
(EXISTS (c: customer, s: taxi_stand):
 (start_waiting_guard(c, s, unprimed))
 AND
 (((waiting_for_cab?(state1(c)(primed)))
   AND (waiting_for_cab_where(c)(primed) = (ref(s))))
  AND
  (((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES (state1(other)(primed) = (state1(other)(unprimed)))))
   AND
   ((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES
     (waiting_for_cab_where(other)(primed)
      = (waiting_for_cab_where(other)(unprimed))))))))
AND
(((FORALL (other: customer):
   state2(other)(primed) = (state2(other)(unprimed))))
 AND
 (((FORALL (other: customer):
    in_cab_which(other)(primed) = (in_cab_which(other)(unprimed))))
  AND
  (((FORALL (other: cab): state4(other)(primed) = (state4(other)(unprimed))))
   AND
   (((FORALL (other: cab): state3(other)(primed) = (state3(other)(unprimed))))
    AND
    ((FORALL (other: cab):
      at_stand_where(other)(primed) = (at_stand_where(other)(unprimed))))))))

end_ride_guard((cb: cab), (c: customer), (other: state)): bool =
(in_cab?(state2(c)(other)))
AND
((in_cab_which(c)(other) = ref(cb))
 AND
 (((on_the_road_engaged?(state3(cb)(other)))
   AND (on_the_road?(state4(cb)(other))))
  AND (being_served?(state1(c)(other)))))

end_ride((unprimed, primed: state)): bool =
(EXISTS (cb: cab, c: customer):
 (end_ride_guard(cb, c, unprimed))
 AND
 (((outside?(state2(c)(primed)))
   AND
   ((on_the_road?(state4(cb)(primed)))
    AND
    ((on_the_road_free?(state3(cb)(primed))) AND (idle?(state1(c)(primed))))))
  AND
  (((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES (state1(other)(primed) = (state1(other)(unprimed)))))
   AND
   (((FORALL (other: customer):
      ((other) /= (c))
      IMPLIES
      (waiting_for_cab_where(other)(primed)
       = (waiting_for_cab_where(other)(unprimed)))))
    AND
    (((FORALL (other: customer):
       ((other) /= (c))
       IMPLIES (state2(other)(primed) = (state2(other)(unprimed)))))
     AND
     (((FORALL (other: customer):
        ((other) /= (c))
        IMPLIES
        (in_cab_which(other)(primed) = (in_cab_which(other)(unprimed)))))
      AND
      (((FORALL (other: cab):
         ((other) /= (cb))
         IMPLIES (state4(other)(primed) = (state4(other)(unprimed)))))
       AND
       (((FORALL (other: cab):
          ((other) /= (cb))
          IMPLIES (state3(other)(primed) = (state3(other)(unprimed)))))
        AND
        ((FORALL (other: cab):
          ((other) /= (cb))
          IMPLIES
          (at_stand_where(other)(primed)
           = (at_stand_where(other)(unprimed)))))))))))))
AND TRUE

enter_stand_guard((cb: cab), (s: taxi_stand), (other: state)): bool =
((on_the_road_free?(state3(cb)(other))) AND (on_the_road?(state4(cb)(other))))
AND (on_the_road?(state4(cb)(other)))

enter_stand((unprimed, primed: state)): bool =
(EXISTS (cb: cab, s: taxi_stand):
 (enter_stand_guard(cb, s, unprimed))
 AND
 (((at_stand?(state4(cb)(primed))) AND (at_stand_where(cb)(primed) = (ref(s))))
  AND
  (((FORALL (other: cab):
     ((other) /= (cb))
     IMPLIES (state4(other)(primed) = (state4(other)(unprimed)))))
   AND
   (((FORALL (other: cab):
      ((other) /= (cb))
      IMPLIES (state3(other)(primed) = (state3(other)(unprimed)))))
    AND
    ((FORALL (other: cab):
      ((other) /= (cb))
      IMPLIES
      (at_stand_where(other)(primed)
       = (at_stand_where(other)(unprimed)))))))))
AND
(((FORALL (other: customer):
   state1(other)(primed) = (state1(other)(unprimed))))
 AND
 (((FORALL (other: customer):
    waiting_for_cab_where(other)(primed)
    = (waiting_for_cab_where(other)(unprimed))))
  AND
  (((FORALL (other: customer):
     state2(other)(primed) = (state2(other)(unprimed))))
   AND
   ((FORALL (other: customer):
     in_cab_which(other)(primed) = (in_cab_which(other)(unprimed)))))))

get_service_guard((c: customer), (other: state)):
bool = FALSE AND (waiting_for_cab?(state1(c)(other)))

get_service((unprimed, primed: state)): bool =
(EXISTS (c: customer):
 (get_service_guard(c, unprimed))
 AND
 ((being_served?(state1(c)(primed)))
  AND
  (((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES (state1(other)(primed) = (state1(other)(unprimed)))))
   AND
   ((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES
     (waiting_for_cab_where(other)(primed)
      = (waiting_for_cab_where(other)(unprimed))))))))
AND
(((FORALL (other: customer):
   state2(other)(primed) = (state2(other)(unprimed))))
 AND
 (((FORALL (other: customer):
    in_cab_which(other)(primed) = (in_cab_which(other)(unprimed))))
  AND
  (((FORALL (other: cab): state4(other)(primed) = (state4(other)(unprimed))))
   AND
   (((FORALL (other: cab): state3(other)(primed) = (state3(other)(unprimed))))
    AND
    ((FORALL (other: cab):
      at_stand_where(other)(primed) = (at_stand_where(other)(unprimed))))))))

stop_waiting_guard((c: customer), (other: state)):
bool = waiting_for_cab?(state1(c)(other))

stop_waiting((unprimed, primed: state)): bool =
(EXISTS (c: customer):
 (stop_waiting_guard(c, unprimed))
 AND
 ((idle?(state1(c)(primed)))
  AND
  (((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES (state1(other)(primed) = (state1(other)(unprimed)))))
   AND
   ((FORALL (other: customer):
     ((other) /= (c))
     IMPLIES
     (waiting_for_cab_where(other)(primed)
      = (waiting_for_cab_where(other)(unprimed))))))))
AND
(((FORALL (other: customer):
   state2(other)(primed) = (state2(other)(unprimed))))
 AND
 (((FORALL (other: customer):
    in_cab_which(other)(primed) = (in_cab_which(other)(unprimed))))
  AND
  (((FORALL (other: cab): state4(other)(primed) = (state4(other)(unprimed))))
   AND
   (((FORALL (other: cab): state3(other)(primed) = (state3(other)(unprimed))))
    AND
    ((FORALL (other: cab):
      at_stand_where(other)(primed) = (at_stand_where(other)(unprimed))))))))

exit_stand_guard((cb: cab), (other: state)):
bool = at_stand?(state4(cb)(other))

exit_stand((unprimed, primed: state)): bool =
(EXISTS (cb: cab):
 (exit_stand_guard(cb, unprimed))
 AND
 (((on_the_road?(state4(cb)(primed)))
   AND
   (state3(cb)(primed)
    = IF on_the_road?(state4(cb)(primed))
    AND NOT on_the_road?(state4(cb)(unprimed)) THEN on_the_road_free
    ELSE state3(cb)(unprimed)
    ENDIF))
  AND
  (((FORALL (other: cab):
     ((other) /= (cb))
     IMPLIES (state4(other)(primed) = (state4(other)(unprimed)))))
   AND
   (((FORALL (other: cab):
      ((other) /= (cb))
      IMPLIES (state3(other)(primed) = (state3(other)(unprimed)))))
    AND
    ((FORALL (other: cab):
      ((other) /= (cb))
      IMPLIES
      (at_stand_where(other)(primed)
       = (at_stand_where(other)(unprimed)))))))))
AND
(((FORALL (other: customer):
   state1(other)(primed) = (state1(other)(unprimed))))
 AND
 (((FORALL (other: customer):
    waiting_for_cab_where(other)(primed)
    = (waiting_for_cab_where(other)(unprimed))))
  AND
  (((FORALL (other: customer):
     state2(other)(primed) = (state2(other)(unprimed))))
   AND
   ((FORALL (other: customer):
     in_cab_which(other)(primed) = (in_cab_which(other)(unprimed)))))))

END rides
Pertti Kellomäki (pk@cs.tut.fi)
Give feedback.