| Summary: | Faulty strategy caused by invariants | ||
|---|---|---|---|
| Product: | UPPAAL TIGA | Reporter: | Christian Ovesen <chresser_900> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | major | ||
| Priority: | P5 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Windows 10 | ||
| Architecture: | |||
| Attachments: | A model with two templates: S and M | ||
Created attachment 322 [details] A model with two templates: S and M Observed: If we perform the following query "Refinement: M<=S" on the attached model with verifytga, we get "property not satisfied" and the following strategy: Strategy for the attacker: State: ( S.L1 M.L1 ) [spoiler] While you are in (S.x<=5 && S.x==M.x), wait. When you are in (5<S.x && S.x==M.x), take transition S.L1->S.L2 { x >= 3, c?, 1 } State: ( S.L2 M.L1 ) [spoiler] While you are in (S.x==M.x), wait. State: ( S.L0 M.L0 ) [spoiler] When you are in true, take transition M.L0->M.L1 { 1, b!, x := 0 } [SKIP] The strategy for state S.L1 M.L1 suggest to take transition S.L1->S.L2 when 5<S.x, however there is an invariant x<=5 on S.L2 which is violated if we perform this transition. Expected: The engine should respond with the following strategy instead: Strategy for the attacker: State: ( S.L0 M.L0 ) [spoiler] When you are in true, take transition M.L0->M.L1 { 1, b!, x := 0 } [SKIP] State: ( S.L2 M.L1 ) [spoiler] While you are in (S.x==M.x), wait. Steps: 1. Open commandopromt 2. Type following command: <verifytga> -t0 <model.xml> <queryfile> to recieve the faulty strategy Build: I tried with the following verifytga version: (Academic) UPPAAL-TIGA 4.1.12-0.16 (rev. 5145), April 2013 Copyright (c) 1995 - 2013, Uppsala University and Aalborg University. All rights reserved. Compiled with i686-w64-mingw32-g++ -Wall -DLIBXML_STATIC -DNDEBUG -O2 -ffloat-store -msse2 -m32 -march=core2 -DENABLE_TIGA -DMULTI_TERMINAL -DENABLE_STORE_MINGRAPH -DTIGA_MERGE_STATES -DTIGA_GREEDY_MERGE -DTIGA_OTF_BUCHI -DBOOST_DISABLE_THREADS -mwindows Free for academic and non-commercial use only. Frequency: 10/10