Bug #83

64-bit version displays counterexamples even with the -quiet option

Added by Tristan Le Gall over 2 years ago. Updated over 2 years ago.

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.

Also available in: Atom PDF