%Patch files loaded: patch2 version 1.2.2.36

$$$mcdemo.pvs


mcdemo  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING

  S: TYPE = {s0,s1,s2,s3}
  s,next: VAR S

  output: TYPE = [# a, b:bool #]
  T:bool=TRUE
  F:bool=FALSE

  P(s):output = TABLE
|[ 	s=s0	| 	s=s1	| 	s=s2	| 	s=s3	]|
%----------------------------------------------------------------%
|(# a:=T,b:=F #)|(# a:=T,b:=T #)|(# a:=F,b:=T #)|(# a:=F,b:=F #)||
  ENDTABLE

  R(s,next):bool = TABLE
   s,	next
      |[ s0 | s1 | s2 | s3 ]|
  | s0 | F  | T  | T  | F  |
  | s1 | F  | T  | T  | F  |
  | s2 | F  | F  | F  | T  |
  | s3 | F  | F  | F  | F ||
  ENDTABLE

  R1(s,next):bool = (s=s0 AND (next = s1 OR next=s2))
			OR (s=s1 AND (next = s1 OR next=s2))
			OR (s=s2 AND next = s3)
		   

 same: LEMMA R(s,next)=R1(s,next)

 check:THEOREM R(s0,s0)

 f(s):bool = (P(s)=(# a:=F,b:=F #))
 Ff(s):bool = NOT(P(s)=(# a:=T,b:=T #))

 check2:THEOREM EF(R1,f)(s)

 check3:THEOREM AF(R1,f)(s)

 FairCheck3:THEOREM fairAF(R1,f)(Ff)(s)

 check3a:THEOREM s2?(s) => AF(R1,f)(s)

  check4:THEOREM EF(R,f)(s)

  check5:THEOREM s2?(s) OR s3?(s) => AU(R1,TRUE,FALSE)(s)


  END mcdemo



symbolic_mcdemo  : THEORY

  BEGIN

   state: TYPE = [# a, b:bool #]
  s,next: VAR state

  T:bool=TRUE
  F:bool=FALSE

  R1(s,next):bool =    (s`a AND next`b)
	            OR (NOT s`a AND s`b AND NOT next`a AND NOT next`b)
		   

 f(s):bool =  s=(# a:=F, b:=F#)
 Ff(s):bool = NOT(s=(# a:=T,b:=T #))

 check2:THEOREM EF(R1,f)(s)

 check3:THEOREM AF(R1,f)(s)

 FairCheck3:THEOREM fairAF(R1,f)(Ff)(s)

 s2?(s):bool = s=(# a:=F, b:=T #)

 check3a:THEOREM s2?(s) => AF(R1,f)(s)


  check5:THEOREM NOT s`a => AU(R1,TRUE,FALSE)(s)


  END symbolic_mcdemo



$$$mcdemo.prf
(|mcdemo| (P_TCC1 "" (COND-DISJOINT-TCC) NIL NIL)
 (P_TCC2 "" (COND-COVERAGE-TCC) NIL NIL) (R_TCC1 "" (CASES-TCC))
 (|same| "" (SKOLEM!) (("" (POSTPONE) NIL NIL)) NIL)
 (|check| "" (POSTPONE) NIL NIL) (|check2| "" (MODEL-CHECK) NIL NIL)
 (|check3| "" (AUTO-REWRITE-THEORIES "mcdemo")
  (("" (MODEL-CHECK) (("" (POSTPONE) NIL NIL)) NIL)) NIL)
 (|FairCheck3| "" (MODEL-CHECK) NIL NIL) (|check3a| "" (MODEL-CHECK) NIL NIL)
 (|check4| "" (EXPAND "R")
  (("" (AUTO-REWRITE-THEORIES "mcdemo")
    (("" (ASSERT)
      (("" (MODEL-CHECK) (("1" (POSTPONE) NIL NIL) ("2" (POSTPONE) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|check5| "" (MODEL-CHECK) NIL NIL))
(|symbolic_mcdemo| (|check2| "" (MODEL-CHECK) NIL NIL)
 (|check3| "" (MODEL-CHECK) (("" (POSTPONE) NIL NIL)) NIL)
 (|FairCheck3| "" (MODEL-CHECK) NIL NIL) (|check3a| "" (MODEL-CHECK) NIL NIL)
 (|check5| "" (MODEL-CHECK) NIL NIL))