Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

# PVS Bug 369

Synopsis:        model-check
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Oct 28 11:00:02 1999
Originator:      mokkedem
Organization:    segsrv.hlo.dec.com
Release:         PVS 2.3
Environment:
System:
Architecture:

Description:

Hi,

the following theory is not modelcheckable, even though the state is finite.

Quite interesting, when you replace length with 2 in  seq: [below[length] ->
bool]
it becomes modelcheckable.

abdel

% ------------- not modelcheckable ----------------------

mctest : THEORY

BEGIN

myfinseq2: TYPE = [# length: below[2], seq: [below[length] -> bool] #]

State : TYPE = [# x : {n : nat | n <= 2}, y : myfinseq2 #]

trans(s,s_n : State) : bool = x(s_n) = IF x(s) = 2 THEN 0 ELSE x(s) + 1 ENDIF

inv(s:State) : bool = x(s) <= 2

IMPORTING ctlops[State]

thm : THEOREM FORALL (s:State) : AG(trans,inv)(s)

END mctest

% ------------- modelcheckable ----------------------

mctest : THEORY

BEGIN

myfinseq2: TYPE = [# length: below[2], seq: [below[2] -> bool] #]

State : TYPE = [# x : {n : nat | n <= 2}, y : myfinseq2 #]

trans(s,s_n : State) : bool = x(s_n) = IF x(s) = 2 THEN 0 ELSE x(s) + 1 ENDIF

inv(s:State) : bool = x(s) <= 2

IMPORTING ctlops[State]

thm : THEOREM FORALL (s:State) : AG(trans,inv)(s)

END mctest

How-To-Repeat:

Fix:
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools