Bug #83
64-bit version displays counterexamples even with the -quiet option
Status: | Closed | Start date: | 08/21/2014 | |
---|---|---|---|---|
Priority: | Normal | Due date: | ||
Assignee: | Grégoire Sutre | % Done: | 0% |
|
Category: | - | |||
Target version: | 1.x |
Description
Submitted by Ivan Beschastnikh
options: -quiet and -no-validation
Running on the attached abp.scm, the output of the 32-bit version is:
McScM 1.2.1 - Model Checking Tool,
Model: 16 locations, 64 transitions, 1/1 init/error symbolic states,
CEGAR: 2 loops, 17 nodes, 69 edges,
Result: Model is unsafe (1).
The output of the 64-bit version also includes the counter-example:
McScM 1.2.1 - Model Checking Tool,
Model: 16 locations, 64 transitions, 1/1 init/error symbolic states,
CEGAR: 2 loops, 17 nodes, 69 edges,
Result: Model is unsafe (1).,
Counterexample:,
sender_0xreceiver_0 » |- 1 ! i -| » sender_0xreceiver_1,
[owner=receiver,C]
History
Updated by Grégoire Sutre over 2 years ago
- Status changed from New to Closed
- Assignee changed from Tristan Le Gall to Grégoire Sutre
- Target version set to 1.x
The submitter was apparently using a customized version. He could not reproduce the bug with the official mcscm-1.2.1.Linux_amd64.tar.bz2.