[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: problem with prover



I have enclosed chunnel.pvs. The problem arises when i try to prove the
lemma "loopy". I initially tried to (expand "index") but it comes back
with 'no change'. Why? I also tried to (expand "train1") but again 'no
change'. This makes no sense to me??
-- 
_________________________________________________________________________
Richard Botting                         tel: +44 141 339 8855 ext. 8335
Computing Science                      fax: +44 141 330 4913
University of Glasgow                email: rmb@dcs.gla.ac.uk
Glasgow G12 8QQ                
SCOTLAND                              
__________________________________________________________________________

defs: THEORY
  BEGIN
  
 

  person_name: NONEMPTY_TYPE
  
  current_indication_values: NONEMPTY_TYPE
  
  mode_values: NONEMPTY_TYPE
  
  train_name: NONEMPTY_TYPE
  
  track_no: NONEMPTY_TYPE
  
  collision_values: TYPE = {collision, no_collision}
  
  condition_status_values: TYPE = {condition_defect, condition_ok}
  
  direction_values: TYPE = {low_to_high, high_to_low}
  
  cp_state: TYPE = {cp_open, cp_closed}
  
  END defs


points: THEORY
  BEGIN
  
  ASSUMING
    
    IMPORTING finite_sequences
    
    point_values: TYPE = finseq[real]
    
    points_ax: AXIOM
        FORALL (mpv: point_values):
          length(mpv) >= 2
              AND (FORALL (i: nat): member(i, {n: nat | n <= length(mpv) - 2}) IMPLIES seq(mpv)(i) > seq(mpv)(i + 1))
    
    ENDASSUMING
  
  END points


Position: THEORY
  BEGIN
  
  ASSUMING
    
    IMPORTING points
    
    block: TYPE = [real, real]
    
    blocks: TYPE = finseq[block]
    
    blocks_ax: AXIOM
        FORALL (b: blocks): (length(b) /= 0 AND (FORALL (i: nat): 
          member(i, {n: nat | n <= length(b) - 2}) IMPLIES PROJ_2(seq(b)(i)) = PROJ_1(seq(b)(i + 1))))
    
    ENDASSUMING
  
  END Position


Train: THEORY
  BEGIN
  
  IMPORTING Position, defs
  
  train:
      TYPE =
        [# name: train_name,
           position: blocks,
           max_length: posnat,
           collision_status: collision_values,
           speed: nat,
           direction: direction_values,
           mode: mode_values,
           condition_status: condition_status_values #]
  
  come_to_stop((t1: train)): train = t1 WITH [speed := 0]
  
  in_collision((t1: train)): train = t1 WITH [collision_status := collision]

  change_action((t1: train), (action?: mode_values)): train = t1 WITH [mode := action?]
  
  END Train


my_sequence_ops[T: TYPE]: THEORY    % remember: finite sequences are defined as records.
  BEGIN
  
   IMPORTING finite_sequences[T]

   finseq1: TYPE = { fs: finseq[T] | length(fs) /= 0 }
  
  sub_seq((fs1: finseq[T]), (fs2: finseq[T])): bool =
    length(fs1) <= length(fs2)
        AND EXISTS (j: nat):
        (j <= length(fs2) - length(fs1) AND (FORALL (i: nat): i < length(fs1) IMPLIES seq(fs1)(i) = seq(fs2)(j + i)))
  
  in_seq((t: T), (fs: finseq[T])): bool = EXISTS (i: below(length(fs))): t = seq(fs)(i)

  last((fs: finseq1)): T =  seq(fs)(length(fs) - 1)
  
  head((fs: finseq1)): T = seq(fs)(0)
  
  tail((fs: finseq[T])): finseq[T] = IF length(fs) = 0 THEN fs
                                     ELSE ^( fs, (1, length(fs) - 1)) 
                                     ENDIF
  
  front((fs: finseq[T])): finseq[T] = IF length(fs) = 0 THEN fs
                                      ELSIF length(fs) = 1 THEN empty_seq
                                      ELSE ^( fs, (0, length(fs) - 2)) 
                                      ENDIF
  
  END my_sequence_ops


Track: THEORY
  BEGIN
  
  ASSUMING
    
    IMPORTING Position, defs, Train, my_sequence_ops
    
    track:
      TYPE =
        [# track_name: track_no,
           points: point_values,
           blocks: blocks,
           trains: setof[train],
           obstruction_position: setof[blocks] #]
    
    track_ax1: AXIOM FORALL (tk: track): length(blocks(tk)) = length(points(tk)) - 1
    
    track_ax2: AXIOM
        FORALL (tk: track), (i: nat):
          member(i, {n: nat | n <= length(points(tk)) - 2})
              IMPLIES
            (PROJ_1(finseq_appl(blocks(tk))(i)) = finseq_appl(points(tk))(i)
                 AND PROJ_2(finseq_appl(blocks(tk))(i)) = finseq_appl(points(tk))(i + 1))
    
    track_ax3: AXIOM FORALL (tk: track), (b: blocks): member(b, obstruction_position(tk)) IMPLIES sub_seq(b, blocks(tk))
    
    track_ax4: AXIOM FORALL (tk: track), (t: train): member(t, trains(tk)) IMPLIES sub_seq(position(t), blocks(tk))
    
    ENDASSUMING
  
  i: VAR nat

  add_a_train((tk: track), (t?: train)): track = IF member(t?, trains(tk)) THEN tk ELSE tk WITH [trains := add(t?, trains(tk))] ENDIF
  
  
% index works because the block in blocks are unique, so there is a unique index.

  index((tk: track), (b: block | EXISTS (i: below(length(blocks(tk)))): b = finseq_appl(blocks(tk))(i))):
      RECURSIVE nat = (IF b = finseq_appl(blocks(tk))(0) THEN 0 ELSE index(tk WITH [blocks := tail(blocks(tk))], b) + 1 ENDIF)
       MEASURE
         (LAMBDA (tk: track), (b: block | EXISTS (i: below(length(blocks(tk)))): b = finseq_appl(blocks(tk))(i)): length(blocks(tk)))
  
  next_position((tk: track), (t?: train)): blocks =
    IF NOT member(t?, trains(tk)) THEN position(t?)
    ELSE IF direction(t?) = high_to_low AND last(position(t?)) = last(blocks(tk)) THEN position(t?)
      ELSE IF direction(t?) = low_to_high AND head(position(t?)) = head(blocks(tk)) THEN position(t?)
        ELSE IF direction(t?) = high_to_low THEN IF length(position(t?)) = max_length(t?) + 1 THEN tail(position(t?))
            ELSE IF length(position(t?)) = max_length(t?)
                THEN o(position(t?), ^(blocks(tk), (index(tk, last(position(t?))) + 1, index(tk, last(position(t?))) + 1)))
              ELSE position(t?)
              ENDIF
            ENDIF
          ELSE IF direction(t?) = low_to_high THEN IF length(position(t?)) = max_length(t?) + 1 THEN front(position(t?))
              ELSE IF length(position(t?)) = max_length(t?)
                  THEN o(position(t?), ^(blocks(tk), (index(tk, head(position(t?))) - 1, index(tk, head(position(t?))) - 1)))
                ELSE position(t?)
                ENDIF
              ENDIF
            ELSE position(t?)
            ENDIF
          ENDIF
        ENDIF
      ENDIF
    ENDIF

   move1((tk: track), (t?: train | member(t?,trains(tk)) AND speed(t?) /= 0)): [track,train] = 
              LET updated_t?: train = t? WITH [position := next_position(tk,t?)] in
              (tk WITH 
              [trains := union({t: train | member(t,trains(tk)) AND t /= t?},
                               {t: train | t = updated_t?}) ],
              updated_t?)
  
   collision_situation((tk: track), (p1?,p2?: blocks)): bool =
             EXISTS (b: block | in_seq(b,blocks(tk))): in_seq(b,p1?) AND in_seq(b,p2?)

   obstruction_in_way?((tk: track), (t?: train | member(t?,trains(tk)))): bool =
            EXISTS (obs_pos: blocks | member(obs_pos,obstruction_position(tk))): 
                                   collision_situation(tk, obs_pos, next_position(tk, t?))

   train_in_way?((tk: track), (t?: train | member(t?,trains(tk)))): bool =
           EXISTS (t2: train | member(t2,trains(tk)) AND t2 /= t?):
                                  collision_situation(tk, next_position(tk, t?), position(t2))

   trains_in_way((tk: track), (t?: train | member(t?,trains(tk)))): setof[train] =
         {t: train | member(t,trains(tk)) AND t /= t? AND collision_situation(tk, next_position(tk, t?), position(t)) }

% move: the train moves a step forward, if there is an obstruction or train in the way
% there is a collision.

   move((tk: track), (t?: train | member(t?,trains(tk)) AND speed(t?) /= 0)): [track,train] =
          IF NOT train_in_way?(tk,t?) AND NOT obstruction_in_way?(tk,t?) THEN move1(tk,t?)
          ELSE let updated_t?: train = PROJ_2(move1(tk,t?)) WITH [collision_status := collision] in
            IF train_in_way?(tk,t?) THEN 
              (PROJ_1(move1(tk,t?)) WITH 
              [trains := union(union(
              {t: train | member(t,trains(tk)) AND t /= t? AND NOT member(t,trains_in_way(tk,t?))},
              {t: train | t = updated_t?}),
              {t: train | FORALL (tt: train): 
                   member(tt,trains_in_way(tk,t?)) AND t = tt WITH [collision_status := collision]})],
              updated_t?)
            ELSE  % obstruction in the way.
              (PROJ_1(move1(tk,t?)) WITH 
              [ trains := union(                               
              {t: train | member(t,trains(tk)) AND t /= t?},
              {t: train | t = updated_t?})],
              updated_t?)
            ENDIF
          ENDIF

  

  END Track


General_Train_System: THEORY
  BEGIN
  
  ASSUMING
    
    IMPORTING Train, Track, finite_sets@finite_sets[train]
    
    system: TYPE = [# trains: setof[train], tracks: setof[track] #]
    
    system_ax1: AXIOM  % a train is either not on any track or is associated with a unique track.
        FORALL (s: system), (t: train | member(t, trains(s))):
          EXISTS (tk: track | member(tk, tracks(s))): member(t, trains(tk)) IMPLIES
              NOT EXISTS (tk2: track | member(tk2, tracks(s)) AND tk2 /= tk ): member(t, trains(tk2))

    system_ax2: AXIOM  % if a train is associated with a track then its position is on that track.
        FORALL (s: system), (t: train | member(t, trains(s))):
          EXISTS (tk: track | member(tk, tracks(s))): member(t, trains(tk)) IMPLIES
              sub_seq(position(t),blocks(tk))

    ENDASSUMING

    s: VAR system

    s_tracks(s): TYPE = {tk: track | member(tk,tracks(s))}
    s_trains(s): TYPE = {t: train | member(t,trains(s))}

    find_train((trains: setof[train] | nonempty?(trains)), (tn: train_name | EXISTS (t: train): name(t) = tn)): 
       RECURSIVE train =
            LET t = choose(trains) in
             IF name(t) = tn THEN t
             ELSE find_train(remove(t,trains),tn)
             ENDIF
        MEASURE (LAMBDA (trains: setof[train] | nonempty?(trains)), (tn: train_name | EXISTS (t: train): name(t) = tn):
               Card(trains) )                               
                 


    add_train_to_system( s, (t?: train | NOT member(t?,trains(s)))): system = 
            s WITH [trains := add(t?,trains(s))]
 
    remove_train_from_system( s, (t?: s_trains(s))): system = 
            IF EXISTS (tk1: s_tracks(s)): member(t?, trains(tk1)) THEN s 
            ELSE s WITH [trains := remove(t?,trains(s))]
            ENDIF

    add_train_to_track( s, (tk?: s_tracks(s)), (t?: s_trains(s))): system = 
            IF EXISTS (tk1: s_tracks(s)): member(t?, trains(tk1)) THEN s 
            ELSE s WITH [tracks := union(
                                     {tk: s_tracks(s) | tk /= tk?},
                                     {tk: s_tracks(s) | tk = tk? WITH [trains := add(t?,trains(tk?))]})] 
            ENDIF

   remove_train_from_track( s, (tk?: s_tracks(s)), (t?: s_trains(s))): system = 
            IF NOT member(t?,trains(tk?)) THEN s
            ELSE s WITH [tracks := union(
                                     {tk: s_tracks(s) | tk /= tk?},
                                     {tk: s_tracks(s) | tk = tk? WITH [trains := remove(t?,trains(tk?))]})]
            ENDIF

   change_track( s, (tk1?,tk2?: s_tracks(s)), (t?: s_trains(s))): system = 
            IF NOT member(t?, trains(tk1?)) THEN s
            ELSE s WITH [tracks := union(union(
                                     {tk: s_tracks(s) | tk /= tk1? AND tk /= tk2?},
                                     {tk: s_tracks(s) | tk = tk1? WITH [trains := remove(t?,trains(tk1?))]}),
                                     {tk: s_tracks(s) | tk = tk2? WITH [trains := add(t?,trains(tk1?))]})]
            ENDIF


  END General_Train_System




Thedford_scenario: THEORY

  BEGIN

  ASSUMING
   IMPORTING General_Train_System
  ENDASSUMING

   t1,t2: train_name
   tk1: track_no

   mp: point_values = (# length:= 5,
                               seq:= (LAMBDA (n: below(5)):
                                      COND n=0 -> 256 + 1/10,
                                      n=1 -> 254 + 2/10,
                                      n=2 -> 252 + 4/10,
                                      n=3 -> 250 + 8/10,
                                      n=4 -> 249 + 1/10
                                      ENDCOND) #)

   tk1_blocks: blocks = (# length:= 4,
                     seq:= (LAMBDA (n: below(4)):
                            COND n=0 -> (mp(0),mp(1)),
                                 n=1 -> (mp(1),mp(2)),
                                 n=2 -> (mp(2),mp(3)),
                                 n=3 -> (mp(3),mp(4)) 
                            ENDCOND) #)

   mode1: mode_values

   train1: train = (# 
                 name:= t1,
                 position:= (# length:= 1,
                               seq:= (LAMBDA (n: below(1)):
                                      COND n=0 -> (mp(0),mp(1))
                                      ENDCOND) #),
                 max_length:= 1,
                 collision_status:= no_collision,
                 speed:= 100,
                 direction:= high_to_low,
                 mode:= mode1,
                 condition_status:= condition_ok #)

   train2: train = (# 
                 name:= t2,
                 position:= (# length:= 1,
                               seq:= (LAMBDA (n: below(1)):
                                      COND n=0 -> (mp(2),mp(3))
                                      ENDCOND) #),
                 max_length:= 1,
                 collision_status:= no_collision,
                 speed:= 0,
                 direction:= high_to_low,
                 mode:= mode1,
                 condition_status:= condition_ok #)

   track1: track = (#
                 track_name:= tk1,
                 points:= mp,
                 blocks:= tk1_blocks,
                 trains:= {t:train | t=train1 OR t=train2},
                 obstruction_position:= emptyset #)

   speed_lemma: LEMMA
           FORALL (tk: track):
             FORALL (t: train | member(t, trains(tk))):
               speed(t) /= 0 AND NOT train_in_way?(tk,t) AND NOT obstruction_in_way?(tk,t)
                          IMPLIES speed(PROJ_2(move(tk, t))) /= 0     

   member_lemma: LEMMA FORALL (tk: track):
                        FORALL (t: train | member(t, trains(tk))):
                          speed(t) /= 0 IMPLIES member(PROJ_2(move(tk,t)),trains(PROJ_1(move(tk,t))))

   move1_lemma: LEMMA PROJ_2(move(track1,train1)) = train1 WITH [position:= (# length:= 2,
                               seq:= (LAMBDA (n: below(2)):
                                      COND n=0 -> (mp(0),mp(1)),
                                      n=1 -> (mp(1),mp(2))
                                      ENDCOND) #)]

   crash_scenario: THEOREM LET tk1m1: track = PROJ_1(move(track1,train1)),
                               t1m1: train = PROJ_2(move(track1,train1)),
                               tk1m2: track = PROJ_1(move(tk1m1,t1m1)),
                               t1m2: train = PROJ_2(move(tk1m1,t1m1)),
                               tk1m3: track = PROJ_1(move(tk1m2,t1m2)), 
                               t1m3: train = PROJ_2(move(tk1m2,t1m2))
                           in
                               collision_status(t1m3) = collision AND
                               collision_status(find_train(trains(tk1m3),t2)) = collision
                               
  loopy: LEMMA 
  
 ((LAMBDA (n:
                below[1
                          +
                        length(((# length := 4,
                                   seq :=
                                     (LAMBDA (n: below(4)):
                                        COND
                                        n = 0 -> (256 + 1 / 10, 254 + 2 / 10),
                                        n = 1 -> (254 + 2 / 10, 252 + 4 / 10),
                                        n = 2 -> (252 + 4 / 10, 250 + 8 / 10),
                                        ELSE -> (250 + 8 / 10, 249 + 1 / 10)
                                        ENDCOND)
                                   #)
                                    ^
                                  ((1
                                        +
                                      index((# track_name := tk1,
                                               points :=
                                                 (# length := 5,
                                                    seq :=
                                                      (LAMBDA (n: below(5)):
                                                         COND
                                                         n = 0 ->
                                                         256 + 1 / 10,
                                                         n = 1 ->
                                                         254 + 2 / 10,
                                                         n = 2 ->
                                                         252 + 4 / 10,
                                                         n = 3 ->
                                                         250 + 8 / 10,
                                                         ELSE ->
                                                           249 + 1 / 10
                                                         ENDCOND)
                                                    #),
                                               blocks :=
                                                 (# length := 4,
                                                    seq :=
                                                      (LAMBDA (n: below(4)):
                                                         COND
                                                         n = 0 ->
                                                         (256 + 1 / 10,
                                                          254 + 2 / 10),
                                                         n = 1 ->
                                                         (254 + 2 / 10,
                                                          252 + 4 / 10),
                                                         n = 2 ->
                                                         (252 + 4 / 10,
                                                          250 + 8 / 10),
                                                         ELSE ->
                                                           (250 + 8 / 10,
                                                            249 + 1 / 10)
                                                         ENDCOND)
                                                    #),
                                               trains := {t: train | t = train1 OR t = train2},
                                               obstruction_position := emptyset #),
                                            (256 + 1 / 10, 254 + 2 / 10))),
                                   (1
                                        +
                                      index((# track_name := tk1,
                                               points :=
                                                 (# length := 5,
                                                    seq :=
                                                      (LAMBDA (n: below(5)):
                                                         COND
                                                         n = 0 ->
                                                         256 + 1 / 10,
                                                         n = 1 ->
                                                         254 + 2 / 10,
                                                         n = 2 ->
                                                         252 + 4 / 10,
                                                         n = 3 ->
                                                         250 + 8 / 10,
                                                         ELSE ->
                                                           249 + 1 / 10
                                                         ENDCOND)
                                                    #),
                                               blocks :=
                                                 (# length := 4,
                                                    seq :=
                                                      (LAMBDA (n: below(4)):
                                                         COND
                                                         n = 0 ->
                                                         (256 + 1 / 10,
                                                          254 + 2 / 10),
                                                         n = 1 ->
                                                         (254 + 2 / 10,
                                                          252 + 4 / 10),
                                                         n = 2 ->
                                                         (252 + 4 / 10,
                                                          250 + 8 / 10),
                                                         ELSE ->
                                                           (250 + 8 / 10,
                                                            249 + 1 / 10)
                                                         ENDCOND)
                                                    #),
                                               trains := {t: train | t = train1 OR t = train2},
                                               obstruction_position := emptyset #),
                                            (256 + 1 / 10, 254 + 2 / 10))))))]):
          IF n < 1 THEN (256 + 1 / 10, 254 + 2 / 10)
          ELSE COND
            ((n - 1) = 0) -> (254 + 2 / 10, 252 + 4 / 10),
            (n = 2) -> (252 + 4 / 10, 250 + 8 / 10),
            ELSE -> (250 + 8 / 10, 249 + 1 / 10)
            ENDCOND
          ENDIF)
           =
         (LAMBDA (n: below(2)): COND n = 0 -> (256 + 1 / 10, 254 + 2 / 10), ELSE -> (254 + 2 / 10, 252 + 4 / 10) ENDCOND))



  END Thedford_scenario