%Patch files loaded: patch2 version 1.2.2.36

$$$a4.pvs
A4  : THEORY
BEGIN

% Software Eng 734 Assignment4 
% Professor: Mark Lawford
% Author: Jason Hu

% DEFINITION PART 
% This part define the necessary types used in modeling.
% LIGHTSTATE is the possbile state types of the lights.

LIGHTSTATE: TYPE ={RED,YELLOW,GREEN}
lightstate,lightnext: VAR LIGHTSTATE

% TIMERSTATE is the possbile state types of the timer.
TIMERSTATE: TYPE={SHORT,LONG,INIT,RUNNING}
nexttimer:VAR TIMERSTATE

% STATEYPE is the possible state of the whole system, include the timer, 2 light states, car's state.
STATETYPE: TYPE=[#timer:TIMERSTATE,hwylight:LIGHTSTATE,farmlight:LIGHTSTATE,car:bool#]
state,next: VAR STATETYPE

% TIMERCONTROLTYPE is the type of signal from the CONTROLLER to the TIMER. 
% Here we assume if there is nothing to send to the controller, we represent it as NONE.
% And the timer state do not change while it gets nothing.

TIMERCONTROLTYPE: TYPE={START,RESET,NONE}

% LIGHTCONTROLTYPE is the type of the signal from CONTROLLER to the LIGHTs.
% We can model it as TRUE or FALSE.
% But in the real world , the controller should send the CHANGE Command or just do nothing.
% So here we use CHANGE and NONE to represent CHANGE or no command signal from controller.

LIGHTCONTROLTYPE: TYPE={CHANGE,NONE}

% CONTROLTYPE is the record type which indicate the set of the controller signal.
% This must be the output of the controller.
CONTROLTYPE: TYPE=[#TimerControl:TIMERCONTROLTYPE,HwyLightControl:LIGHTCONTROLTYPE,FarmLightControl:LIGHTCONTROLTYPE#]

% Define CAR state machine.

CAR(state,next):bool=TRUE

% Define the Controller. 
% Please refer my written report which gives the whole controller structure.
% The input of the controller should be  
% 1. timer(state) 2. sensor(state) 3. hwylight(state) 4. farmlight(state)
% So input should be state enough, as state includes these infomation with record type.
% The output of the controller should be
% 1. TimerControl 2. LightControls
% So output should be the record type ,too.
P(state):CONTROLTYPE= TABLE
|timer(state)=LONG AND car(state) AND hwylight(state)=GREEN AND farmlight(state)=RED|(#TimerControl:=RESET,HwyLightControl:=CHANGE,FarmLightControl:=NONE#)||
|timer(state)/=INIT AND (timer(state)=LONG OR  NOT car(state)) AND hwylight(state)=RED AND farmlight(state)=GREEN|(#TimerControl:=RESET,HwyLightControl:=NONE,FarmLightControl:=CHANGE#)||
|timer(state)=SHORT AND hwylight(state)=RED AND farmlight(state)=YELLOW|(#TimerControl:=RESET,HwyLightControl:=CHANGE,FarmLightControl:=CHANGE#)||
|timer(state)=SHORT AND hwylight(state)=YELLOW AND farmlight(state)=RED|(#TimerControl:=RESET,HwyLightControl:=CHANGE,FarmLightControl:=CHANGE#)||
|timer(state)=INIT AND hwylight(state)=RED AND farmlight(state)=RED|(#TimerControl:=START,HwyLightControl:=CHANGE,FarmLightControl:=NONE#)||
|timer(state)=INIT AND NOT(hwylight(state)=RED AND farmlight(state)=RED)|(#TimerControl:=START,HwyLightControl:=NONE,FarmLightControl:=NONE#)||
|ELSE|(#TimerControl:=NONE,HwyLightControl:=NONE,FarmLightControl:=NONE#)||
ENDTABLE

% Define the TIMER state machine model
% With the output of the controller's TimerControl section
% we can define it as followings.

TIMER(state,next):bool=TABLE
|timer(state)=INIT AND TimerControl(P(state))=START AND timer(next)=RUNNING|TRUE||
|timer(state)=RUNNING AND TimerControl(P(state))=NONE AND (timer(next)=RUNNING OR timer(next)=SHORT)|TRUE||
|timer(state)=SHORT AND TimerControl(P(state))=NONE AND (timer(next)=SHORT OR timer(next)=LONG)|TRUE||
|timer(state)=LONG AND TimerControl(P(state))=NONE AND timer(next)=LONG|TRUE||
|TimerControl(P(state))=RESET AND timer(next)=INIT|TRUE||
|TimerControl(P(state))=NONE AND timer(state)=timer(next)|TRUE||
|ELSE|FALSE||
ENDTABLE

% Highway light state machine model
HWYLIGHT(state,next):bool=TABLE
|hwylight(state)=RED and HwyLightControl(P(state))=CHANGE and hwylight(next)=GREEN|TRUE||
|hwylight(state)=GREEN and HwyLightControl(P(state))=CHANGE and hwylight(next)=YELLOW|TRUE||
|hwylight(state)=YELLOW and HwyLightControl(P(state))=CHANGE and hwylight(next)=RED|TRUE||
|HwyLightControl(P(state))=NONE and hwylight(next)=hwylight(state)|TRUE||
|ELSE|FALSE||
ENDTABLE

% Farm light state machine model 
FARMLIGHT(state,next):bool=TABLE
|farmlight(state)=RED and FarmLightControl(P(state))=CHANGE and farmlight(next)=GREEN|TRUE||
|farmlight(state)=GREEN and FarmLightControl(P(state))=CHANGE and farmlight(next)=YELLOW|TRUE||
|farmlight(state)=YELLOW and FarmLightControl(P(state))=CHANGE and farmlight(next)=RED|TRUE||
|FarmLightControl(P(state))=NONE and farmlight(next)=farmlight(state)|TRUE||
|ELSE|FALSE||
ENDTABLE

% Initial state definition.
% Please refer the written report for initial state.
init(state):bool=(state=(#timer:=INIT,hwylight:=RED,farmlight:=RED,car:=TRUE#) OR state=(#timer:=INIT,hwylight:=RED,farmlight:=RED,car:=FALSE#))


% Whole system definition. Here I use the sycronization mode.
R(state,next):bool=HWYLIGHT(state,next) AND FARMLIGHT(state,next) AND TIMER(state,next) AND CAR(state,next)

% Question 5 

% Check there should not be 2 green lights at same time. 
check1: THEOREM init(state) IMPLIES AG(R,NOT (hwylight(state)= GREEN AND farmlight(state)=GREEN))(state)

% Check there should not be yellow and green at same time.
check3: THEOREM init(state) IMPLIES AG(R,NOT (hwylight(state)= GREEN AND farmlight(state)=YELLOW))(state)

% Check Next state of the farm light. Can not prove BadTest.
GoodTest:THEOREM init(state) => AX(R, farmlight(state)=RED)(state)
BadTest:THEOREM init(state) => AX(R, farmlight(state)/=RED)(state)

% Check farm light
GoodTest2:THEOREM init(state)=> EF(R, (lambda(q:STATETYPE):farmlight(q)=GREEN))(state) AND EF(R, (lambda(r:STATETYPE):farmlight(r)=YELLOW))(state)

% Check timer
GoodTest21:THEOREM init(state)=> EF(R, (lambda(q:STATETYPE):timer(q)=SHORT))(state) 
GoodTest22:THEOREM init(state)=> EF(R, (lambda(q:STATETYPE):timer(q)=LONG))(state)

% Check all impossible light states. 
checklights: THEOREM init(state) =>
           AG(R,lambda(q:STATETYPE):NOT(hwylight(q)=GREEN AND farmlight(q)=GREEN OR
                                      hwylight(q)=YELLOW AND farmlight(q)=YELLOW OR
                                      hwylight(q)=GREEN AND farmlight(q)=YELLOW OR
                                      hwylight(q)=YELLOW AND farmlight(q)=GREEN))(state)


%Question 6 
Ff(state):bool = NOT(timer(state)=RUNNING) AND NOT(timer(state)=SHORT)

Q6a: THEOREM init(state) IMPLIES (fairAG(R,(lambda(q:STATETYPE):car(q) AND timer(q)=LONG))(Ff)(state) IMPLIES fairAF(R,(lambda(r:STATETYPE):farmlight(r)=GREEN))(Ff)(state))

Q6b:THEOREM  init(state) =>  fairAG(R, fairAF(R,(lambda(r:STATETYPE): hwylight(r)=GREEN))(Ff))(Ff)(state)


% Additional Check
% Regarding Professor Lawford's email.

check72: THEOREM init(state) IMPLIES (fairAG(R, (lambda(q:STATETYPE):car(q) AND farmlight(q)=RED))(Ff)(state) => fairAX(R,(lambda(r:STATETYPE): farmlight(r)=GREEN))(Ff)(state))

GoodTest6:THEOREM init(state)=> fairEF(R, (lambda(q:STATETYPE):farmlight(q)=GREEN))(Ff)(state)

%Create a fairness condition to basically force consideration of paths where car is present for two consecutive states infinite number of times
Ff1(state):bool = car(state) AND NOT(timer(state)=RUNNING) AND NOT(timer(state)=SHORT)
GoodTest42:THEOREM  init(state) =>  fairAG(R, fairAF(R,(lambda(r:STATETYPE): farmlight(r)=GREEN))(Ff1))(Ff1)(state)

END A4









$$$a4.prf
(A4 (P_TCC1 "" (COND-DISJOINT-TCC) NIL NIL)
 (|check1| "" (MODEL-CHECK) NIL NIL)
 (|check3| "" (MODEL-CHECK) NIL NIL)
 (|GoodTest| "" (MODEL-CHECK) NIL NIL)
 (|BadTest| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)
   ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
   ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL) ("9" (GRIND) NIL NIL)
   ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL) ("12" (GRIND) NIL NIL)
   ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL) ("15" (GRIND) NIL NIL)
   ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL) ("18" (GRIND) NIL NIL)
   ("19" (GRIND) NIL NIL) ("20" (GRIND) NIL NIL) ("21" (GRIND) NIL NIL)
   ("22" (GRIND) NIL NIL) ("23" (GRIND) NIL NIL) ("24" (GRIND) NIL NIL)
   ("25" (GRIND) NIL NIL) ("26" (GRIND) NIL NIL)
   ("27" (GRIND)
    (("27" (GRIND)
      (("27" (GRIND)
        (("27" (GRIND) (("27" (GRIND) (("27" (POSTPONE) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   ("28" (POSTPONE) NIL NIL) ("29" (POSTPONE) NIL NIL)
   ("30" (POSTPONE) NIL NIL) ("31" (POSTPONE) NIL NIL)
   ("32" (POSTPONE) NIL NIL) ("33" (POSTPONE) NIL NIL)
   ("34" (POSTPONE) NIL NIL) ("35" (POSTPONE) NIL NIL)
   ("36" (POSTPONE) NIL NIL))
  NIL)
 (|GoodTest2| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)
   ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
   ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL) ("9" (GRIND) NIL NIL)
   ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL) ("12" (GRIND) NIL NIL)
   ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL) ("15" (GRIND) NIL NIL)
   ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL))
  NIL)
 (|GoodTest21| "" (MODEL-CHECK)
  (("1" (MODEL-CHECK) NIL NIL) ("2" (GRIND) NIL NIL)
   ("3" (GRIND) NIL NIL) ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL)
   ("6" (GRIND) NIL NIL) ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL)
   ("9" (GRIND) NIL NIL) ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL)
   ("12" (GRIND) NIL NIL) ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL)
   ("15" (GRIND) NIL NIL) ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL)
   ("18" (GRIND) NIL NIL) ("19" (GRIND) NIL NIL) ("20" (GRIND) NIL NIL)
   ("21" (GRIND) NIL NIL) ("22" (GRIND) NIL NIL) ("23" (GRIND) NIL NIL)
   ("24" (GRIND) NIL NIL) ("25" (GRIND) NIL NIL) ("26" (GRIND) NIL NIL)
   ("27" (GRIND) NIL NIL) ("28" (GRIND) NIL NIL) ("29" (GRIND) NIL NIL)
   ("30" (GRIND) NIL NIL) ("31" (GRIND) NIL NIL) ("32" (GRIND) NIL NIL)
   ("33" (GRIND) NIL NIL) ("34" (GRIND) NIL NIL) ("35" (GRIND) NIL NIL)
   ("36" (GRIND) NIL NIL) ("37" (GRIND) NIL NIL) ("38" (GRIND) NIL NIL)
   ("39" (GRIND) NIL NIL) ("40" (GRIND) NIL NIL) ("41" (GRIND) NIL NIL)
   ("42" (GRIND) NIL NIL) ("43" (GRIND) NIL NIL)
   ("44" (GRIND) NIL NIL))
  NIL)
 (|GoodTest22| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)
   ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
   ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL) ("9" (GRIND) NIL NIL)
   ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL) ("12" (GRIND) NIL NIL)
   ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL) ("15" (GRIND) NIL NIL)
   ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL) ("18" (GRIND) NIL NIL)
   ("19" (GRIND) NIL NIL) ("20" (GRIND) NIL NIL) ("21" (GRIND) NIL NIL)
   ("22" (GRIND) NIL NIL) ("23" (GRIND) NIL NIL) ("24" (GRIND) NIL NIL)
   ("25" (GRIND) NIL NIL) ("26" (GRIND) NIL NIL) ("27" (GRIND) NIL NIL)
   ("28" (GRIND) NIL NIL) ("29" (GRIND) NIL NIL) ("30" (GRIND) NIL NIL)
   ("31" (GRIND) NIL NIL) ("32" (GRIND) NIL NIL) ("33" (GRIND) NIL NIL)
   ("34" (GRIND) NIL NIL) ("35" (GRIND) NIL NIL) ("36" (GRIND) NIL NIL)
   ("37" (GRIND) NIL NIL) ("38" (GRIND) NIL NIL) ("39" (GRIND) NIL NIL)
   ("40" (GRIND) NIL NIL) ("41" (GRIND) NIL NIL) ("42" (GRIND) NIL NIL)
   ("43" (GRIND) NIL NIL) ("44" (GRIND) NIL NIL) ("45" (GRIND) NIL NIL)
   ("46" (GRIND) NIL NIL) ("47" (GRIND) NIL NIL) ("48" (GRIND) NIL NIL)
   ("49" (GRIND) NIL NIL) ("50" (GRIND) NIL NIL)
   ("51" (GRIND) NIL NIL))
  NIL)
 (|checklights| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL))
  NIL)
 (|Q6a| "" (MODEL-CHECK) NIL NIL)
 (|Q6b| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)
   ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
   ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL) ("9" (GRIND) NIL NIL)
   ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL) ("12" (GRIND) NIL NIL)
   ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL) ("15" (GRIND) NIL NIL)
   ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL) ("18" (GRIND) NIL NIL)
   ("19" (GRIND) NIL NIL) ("20" (GRIND) NIL NIL) ("21" (GRIND) NIL NIL)
   ("22" (GRIND) NIL NIL) ("23" (GRIND) NIL NIL) ("24" (GRIND) NIL NIL)
   ("25" (GRIND) NIL NIL) ("26" (GRIND) NIL NIL) ("27" (GRIND) NIL NIL)
   ("28" (GRIND) NIL NIL) ("29" (GRIND) NIL NIL) ("30" (GRIND) NIL NIL)
   ("31" (GRIND) NIL NIL) ("32" (GRIND) NIL NIL) ("33" (GRIND) NIL NIL)
   ("34" (GRIND) NIL NIL) ("35" (GRIND) NIL NIL) ("36" (GRIND) NIL NIL)
   ("37" (GRIND) NIL NIL) ("38" (GRIND) NIL NIL) ("39" (GRIND) NIL NIL)
   ("40" (GRIND) NIL NIL))
  NIL)
 (|check72| "" (MODEL-CHECK) NIL NIL)
 (|check7| "" (MODEL-CHECK) NIL NIL)
 (|GoodTest6| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)
   ("4" (GRIND) NIL NIL) ("5" (GRIND) NIL NIL) ("6" (GRIND) NIL NIL)
   ("7" (GRIND) NIL NIL) ("8" (GRIND) NIL NIL) ("9" (GRIND) NIL NIL)
   ("10" (GRIND) NIL NIL) ("11" (GRIND) NIL NIL) ("12" (GRIND) NIL NIL)
   ("13" (GRIND) NIL NIL) ("14" (GRIND) NIL NIL) ("15" (GRIND) NIL NIL)
   ("16" (GRIND) NIL NIL) ("17" (GRIND) NIL NIL) ("18" (GRIND) NIL NIL)
   ("19" (GRIND) NIL NIL) ("20" (GRIND) NIL NIL) ("21" (GRIND) NIL NIL)
   ("22" (GRIND) NIL NIL) ("23" (GRIND) NIL NIL) ("24" (GRIND) NIL NIL)
   ("25" (GRIND) NIL NIL) ("26" (GRIND) NIL NIL) ("27" (GRIND) NIL NIL)
   ("28" (GRIND) NIL NIL) ("29" (GRIND) NIL NIL) ("30" (GRIND) NIL NIL)
   ("31" (GRIND) NIL NIL) ("32" (GRIND) NIL NIL) ("33" (GRIND) NIL NIL)
   ("34" (GRIND) NIL NIL) ("35" (GRIND) NIL NIL) ("36" (GRIND) NIL NIL)
   ("37" (GRIND) NIL NIL) ("38" (GRIND) NIL NIL) ("39" (GRIND) NIL NIL)
   ("40" (GRIND) NIL NIL) ("41" (GRIND) NIL NIL) ("42" (GRIND) NIL NIL)
   ("43" (GRIND) NIL NIL))
  NIL)
 (|GoodTest42| "" (MODEL-CHECK)
  (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL))
  NIL))