Visualisation of CVC cores in STG model

Cores can be obtained from MPSat output. Each core is a separate solution comprising two traces. The transitions in the core are calculated as a difference between the sets of transitions in the two sets of the solution.

$ ./punf_pnml stg-vme.g

 Net file: stg-vme.g
 The number of working threads: 4
 Total SAT time: 0.00
 2QBF main/aux/total time: 0.00/0.00/0.00
 2QBF qbf/main/aux calls: 0/0/0
 Average blocking clause length: 0.00

$ ./mpsat_pnml -C -a stg-vme.bp.pnml.gz

file: stg-vme.bp.pnml.gz
 |B|=26 |E|=22 |C|=3 |BE|=26 |EB|=24
SOLUTION 0:
DSw+, D+/1, LDS+/1, LDTACK+/1
DSr+, LDS+, LDTACK+, D+, DTACK+, DSr-, D-, DTACK-, DSw+, D+/1
total cost of all paths: 14

Conflict for signal D

SOLUTION 1:
DSr+, LDS+, LDTACK+
DSr+, LDS+, LDTACK+, D+, DTACK+, DSr-, D-, DTACK-, DSr+
total cost of all paths: 12

Conflict for signal D

SOLUTION 2:
DSw+, D+/1, LDS+/1, LDTACK+/1, D-/1
DSr+, LDS+, LDTACK+, D+, DTACK+, DSr-, D-, DTACK-, DSw+
total cost of all paths: 14

Conflict for signal D

CSC conflict has been detected

Original Num Var/Cl/Lit 115/242/714