search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 30 forks source link

Checking for invariants crashes symbolic tool #128

Closed alaarman closed 6 years ago

alaarman commented 7 years ago

Regardless of the MDD that I use, I get: (the invariant is a state label. Can this be the cause?)

$ prom2lts-sym -rbcm,gs --vset=lddmc concrete.prm.spins --invariant=" ! proposed0"

Lace warning: hwloc_set_cpubind returned -1! Lace warning: hwloc_set_cpubind returned -1! Lace warning: hwloc_set_cpubind returned -1! Lace warning: hwloc_set_cpubind returned -1! Lace error: Unable to bind worker memory to node! Lace error: Unable to bind worker memory to node! Lace error: Unable to bind worker memory to node! Lace error: Unable to bind worker memory to node! Lace warning: hwloc_get_area_membind_nodeset returned -1! Lace warning: hwloc_get_area_membind_nodeset returned -1! Lace warning: hwloc_get_area_membind_nodeset returned -1! Lace warning: hwloc_get_area_membind_nodeset returned -1! Lace warning: Lace worker memory not bound with BIND policy! Lace warning: Lace worker memory not bound with BIND policy! Lace warning: Lace worker memory not bound with BIND policy! Lace warning: Lace worker memory not bound with BIND policy! prom2lts-sym: Exploration order is bfs-prev prom2lts-sym: Saturation strategy is none prom2lts-sym: Guided search strategy is unguided prom2lts-sym: Attractor strategy is default prom2lts-sym: Precompiled SpinS module initialized prom2lts-sym: opening concrete.prm.spins prom2lts-sym: Initializing regrouping layer prom2lts-sym: Regroup specification: bcm,gs prom2lts-sym: Regroup Boost's Cuthill McKee prom2lts-sym: Regroup macro Group Safely: gc,gr,cw,rs prom2lts-sym: Regroup macro Cols: cs,cn prom2lts-sym: Regroup Column Sort prom2lts-sym: Regroup Column Nub prom2lts-sym: Regroup macro Rows: rs,rn prom2lts-sym: Regroup Row Sort prom2lts-sym: Regroup Row Nub prom2lts-sym: Regroup Column sWaps prom2lts-sym: Regroup Row Sort prom2lts-sym: Regrouping: 224->70 groups prom2lts-sym: Regrouping took 0.020 real 0.020 user 0.010 sys prom2lts-sym: state vector length is 97; there are 70 groups prom2lts-sym: Creating a multi-core ListDD domain. prom2lts-sym: Sylvan allocates 10.500 GB virtual memory for nodes table and operation cache. prom2lts-sym: Initial nodes table and operation cache requires 672.00 MB. prom2lts-sym: Using GBgetTransitionsShortR2W as next-state function prom2lts-sym: got initial state prom2lts-sym: level 0 is finished prom2lts-sym: level 1 is finished prom2lts-sym: level 2 is finished Assertion failed: (a != lddmc_true), function lddmc_minus_WORK, file /Users/laarman/Workspace/ltsmin/sylvan/src/sylvan_ldd.c, line 564. Abort trap: 6

Meijuh commented 7 years ago

Can you add concrete.prm?

alaarman commented 7 years ago

concrete.prm.zip

Meijuh commented 7 years ago

I can not compile that promela model, I get the error: SpinS Promela Compiler - version 1.1 (3-Feb-2015) (C) University of Twente, Formal Methods and Tools group

Parsing concrete.prm... Parse exception in file concrete.prm: Encountered " "}" "} "" at line 99, column 1. Was expecting one of: ";" ... "->" ...

Compilation of concrete.prm failed

alaarman commented 6 years ago

apparently a sylvan issue that seems resolved in 1.1.2.