Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

Synopsis: abstract/modelcheck bug Severity: serious Priority: medium Responsible: shankar State: open Class: sw-bug Arrival-Date: Mon Jul 23 20:20:03 2001 Originator: Oliver Moeller Organization: brics.dk Release: PVS 2.3 Environment: System: Architecture: Description: Hi, I think I hit a bug in the abstract/model-check part of PVS Version 2.3 Beta (patch level 1.2.2.176) - Allegro CL Professional Edition 5.0 [Linux/X86] (9/4/99 2:05) In the following example, BOTH properties 'reachB' and 'notreachB' were provable with the command sequence: (ABSTRACT ("lambda(z:state): z`x = 0" "lambda(z:state): z`y = 0" "lambda(z:state): z`x <= i" "lambda(z:state): z`y <= i" "lambda(z:state): z`x - z`y <= i")) (model-check) The system grow2 mimics a simple timed automaton (here with discrete time). If I did not make a mistake, it should always remain in location A. This example works also, if you replace "i" by - eg. "5". - oli http://www.brics.dk/~omoeller *com-pu-ter*: device to enhance our capability to err. <omoeller@brics.dk> %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Grow2 %% Version: DISCRETE TIME DELAY %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Simple timed automata model with one paramter: %% %% X %% Process: / \ AA1 X %% / \ / \ AA2 %% / \ / \ %% / \ / \ %% x <= i / \----- / \ y <= i %% / ( A ) \ %% X / --+---\ - %% y := 0 \ / | \ -/ %% \ / | \ -/ x := 0 %% \ / | --/ %% \ / | %% X | %% \|/ x>i & y = 0 %% ----- %% ( B ) %% ----- %% %% clock: x,y %% nat: i %% %% Synopsis: %% Abstractions of infinite-discrete-state RT systems %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% @TABLE OF CONTENTS: [TOCD: 07:36 23 Jul 2001] %% %% [1] The Model %% [1.1] Preliminaries %% [1.2] Initial State %% [1.3] Discrete Transitions %% [2] The nature of time %% [3] Transition Relation %% [4] Properties %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% @FILE: grow2.pvs %% @PLACE: SRI; host:falkner %% @FORMAT: Prototype Verification System (PVS) %% @AUTHOR: M. Oliver M'o'ller <omoeller@brics.dk> %% @BEGUN: Mon Jul 23 07:35:21 2001 %% @VERSION: Mon Jul 23 16:33:53 2001 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% grow2: THEORY BEGIN %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [1] The Model %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [1.1] Preliminaries %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% loc: TYPE = {A, B} i: nat state: TYPE = [# pc : loc, x : nnreal, y : nnreal #] s, s1: VAR state %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [1.2] Initial State %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% init(s): bool = s`pc = A AND s`x = 0 AND s`y = 0 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [1.3] Discrete Transitions %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% nextAA1(s,s1): bool = s`pc = A AND s`x <= i AND s1 = s WITH [`y := 0] nextAA2(s,s1): bool = s`pc = A AND s`y <= i AND s1 = s WITH [`x := 0 ] nextAB(s,s1): bool = s`pc = A AND s`x > i AND s`y = 0 AND s1 = s WITH [`pc := B ] %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [2] The nature of time %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% == dense ===================================================== delay(s,s1): bool = EXISTS (delta: posreal): s1 = s WITH [`x := s`x + delta, `y := s`y + delta ] %% == discrete (coarse: step 1) ================================= delay_1(s,s1): bool = s1 = s WITH [`x := s`x + 1, `y := s`y + 1 ] %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [3] Transition Relation %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% next(s,s1): bool = nextAA1(s,s1) OR nextAA2(s,s1) OR nextAB(s,s1) OR delay_1(s,s1) %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% [4] Properties %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% == proven =============================================================== deadlockfree: PROPOSITION init(s) => AG(next, LAMBDA s: EX(next, LAMBDA s1: TRUE)(s))(s) reachB: PROPOSITION init(s) => EF(next, LAMBDA s: s`pc = B)(s) notreachB: PROPOSITION init(s) => AG(next, LAMBDA s: s`pc = A)(s) %% == unproven ============================================================= response: PROPOSITION init(s) => AG(next, LAMBDA s: s`y > 0 => AF(next, LAMBDA s: s`y = 0)(s))( s) % leads to: % --------------------- % [-1] (B_1(abs_s!1)) % [-2] (B_2(abs_s!1)) % [-3] abs_s!1`B_3 % |------- % [1] B?(abs_s!1`pc) % --------------------- END grow2 How-To-Repeat: [davesc, 7/23/01] In the current reworking of the abstractor, this breaks with no method for find-supertype in get-free-state-components. Fix:

Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|