%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 = IF ((s=s0 AND (next = s1 OR next=s2))
			OR (s=s1 AND (next = s1 OR next=s2))
			OR (s=s2 AND next = s3))  THEN TRUE
		    ELSE FALSE
		ENDIF

 check:THEOREM R(s0,s0)

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

 IMPORTING ctlops[S]

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

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

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


  END mcdemo

$$$mcdemo.prf
(|mcdemo| (P_TCC1 "" (COND-DISJOINT-TCC) NIL NIL)
 (P_TCC2 "" (COND-COVERAGE-TCC) NIL NIL) (R_TCC1 "" (CASES-TCC))
 (|check| "" (POSTPONE) NIL NIL) (|check2| "" (MODEL-CHECK) NIL NIL)
 (|check3| "" (AUTO-REWRITE-THEORIES "mcdemo")
  (("" (MODEL-CHECK) (("" (POSTPONE) NIL NIL)) NIL)) NIL)
 (|check4| "" (AUTO-REWRITE-THEORIES "mcdemo") (("" (POSTPONE) NIL NIL)) NIL))