Run McScM without -quiet for x86 Linux Support in CSight

[GoogleCodeExporter]

For CSight, McScM does not output counterexample with x86 binary when option 
-quiet is specified.
We should remove the -quiet flag, which will allow McScM to output the counter 
example. However, extra output will be printed by McScM, so parsing of the 
results will need to change to account for the new outputs.

Currently, CSight expects McScM outputs to be in the format of:
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]

Without -quiet, McScM will output:

McScM 1.2.1 - Model Checking Tool
Model: 16 locations, 64 transitions, 1/1 init/error symbolic states
               Loops        Nodes      Edges    Cex len          k
CEGAR loop:        2   (       17 /       69 /        1 )        0 )

CEGAR: 2 loops, 17 nodes, 69 edges
Result: Model is unsafe (1).
Counterexample:

   sender_0xreceiver_0 » |- 1 ! i -| » sender_0xreceiver_1
      [owner=receiver,C]

The input used to generate these outputs is attached.

Original issue reported on code.google.com by bobyan...@gmail.com on 20 Aug 2014 at 10:26

Attachments:

• abp.scm

[GoogleCodeExporter]

Original comment by bobyan...@gmail.com on 26 Aug 2014 at 6:58

• Changed state: Started

[GoogleCodeExporter]

McScM does not always preserve formatting when printing the Result without 
-quiet

The following output is generated with the attached file:
McScM 1.2.1 - Model Checking Tool
Model: 16 locations, 54 transitions, 1/2 init/error symbolic states
               Loops        Nodes      Edges    Cex len          k
CEGAR loop:        0Result: Model is unsafe (0).
Counterexample:

The Result: is not printed on a new line, as expected.

Original comment by bobyan...@gmail.com on 26 Aug 2014 at 7:20

Attachments:

• simpleConcurrencyStringSuccess.scm

[GoogleCodeExporter]

Fixed and merged to default in revision 9a30f0698560

Original comment by bobyan...@gmail.com on 27 Aug 2014 at 12:32

• Changed state: Fixed