--ltl-semantics=spin not working for edge labels

[Meijuh]

A system without a deadlock should give the same answer with --ltl-semantics=spin, --ltl-semantics=ltsmin.

In the following commandline: pnml2lts-mc example.pnml --ltl='[]<>(action=="t_3_a_1")' --ltl-semantics=ltsmin the ltl formula holds. Which is correct; ("a_1") can always fire in the future. Changing the semantics to spin: pnml2lts-mc example.pnml --ltl='[]<>(action=="t_3_a_1")' --ltl-semantics=spin, the formula does not hold.

Some things that I find peculiar:

• the transition count is only updated if the parallel composition does not deadlock: https://github.com/utwente-fmt/ltsmin/blob/next/src/pins-lib/pins2pins-ltl.c#L306.
• the truth of atomic predicates with edge variables is not updated: https://github.com/utwente-fmt/ltsmin/blob/next/src/pins-lib/pins2pins-ltl.c#L277, i.e. after line https://github.com/utwente-fmt/ltsmin/blob/next/src/pins-lib/pins2pins-ltl.c#L338, the old value of new_ctx.predicate_evals is used.
• Whenever the parallel composition deadlocks, with the example formula given, the following block of code is still executed: https://github.com/utwente-fmt/ltsmin/blob/next/src/pins-lib/pins2pins-ltl.c#L348-L365.

The Petri-net can be found below.

https://gist.github.com/Meijuh/6bc2251c5494c33d89ae127983c13955

[alaarman]

The net doesn't work for me:

$ db pins2lts-mc/pnml2lts-mc example.pnml --ltl='[]<>(action=="t_3_a_1")'
(lldb) target create "pins2lts-mc/pnml2lts-mc" Current executable set to 'pins2lts-mc/pnml2lts-mc' (x86_64). (lldb) settings set -- target.run-args "example.pnml" "--ltl=[]<>(action==\"t_3_a_1\")" (lldb) r Process 53333 launched: '/Users/laarman/Projects/Workspace/ltsmin/src/pins2lts-mc/pnml2lts-mc' (x86_64) pnml2lts-mc( 0/ 4): Loading model from example.pnml pnml2lts-mc( 0/ 4): Edge label is id pnml2lts-mc( 0/ 4): Petri net has 8 places, 7 transitions and 24 arcs pnml2lts-mc( 0/ 4): Petri net processes_0_1_min_lang.dot analyzed pnml2lts-mc( 0/ 4): There are safe places Process 53333 stopped

• thread #2, stop reason = EXC_BAD_ACCESS (code=2, address=0x101101320) frame #0: 0x0000000101101320 -> 0x101101320: addb %al, (%rax) 0x101101322: addb %al, (%rax) 0x101101324: addb (%rax), %al 0x101101326: addb %al, (%rax) thread #3, stop reason = EXC_BAD_ACCESS (code=2, address=0x101211510) frame #0: 0x0000000101211510 -> 0x101211510: addb %al, (%rax) 0x101211512: addb %al, (%rax) 0x101211514: addb (%rax), %al 0x101211516: addb %al, (%rax) thread #4, stop reason = EXC_BAD_ACCESS (code=2, address=0x101017210) frame #0: 0x0000000101017210 -> 0x101017210: addb %al, (%rax) 0x101017212: addb %al, (%rax) 0x101017214: addb (%rax), %al 0x101017216: addb %al, (%rax) thread #5, stop reason = EXC_BAD_ACCESS (code=2, address=0x100713f20) frame #0: 0x0000000100713f20 -> 0x100713f20: addb %al, (%rax) 0x100713f22: addb %al, (%rax) 0x100713f24: addb (%rax), %al 0x100713f26: addb %al, (%rax) (lldb) bt
• thread #2, stop reason = EXC_BAD_ACCESS (code=2, address=0x101101320)
  • frame #0: 0x0000000101101320 frame #1: 0x00007fffce5a5349 libsystem_c.dylib_qsort + 1028 frame #2: 0x000000010000541f pnml2lts-mcinit_groups_of_edge(pn_context=0x0000000101101ea0) at pnml-pins.c:822 frame #3: 0x0000000100005f2d pnml2lts-mcset_dependencies(model=0x0000000101200190) at pnml-pins.c:946 frame #4: 0x0000000100006cf9 pnml2lts-mcPNMLloadGreyboxModel(model=0x0000000101200190, name="example.pnml") at pnml-pins.c:1113 frame #5: 0x000000010002d64c pnml2lts-mcGBloadFile(model=0x0000000101200190, filename="example.pnml", wrapped=0x000070000e13de30) at pins.c:1274 frame #6: 0x0000000100001043 pnml2lts-mccreate_pins_model at pins2lts-mc.c:122 frame #7: 0x0000000100001070 pnml2lts-mcglobal_and_model_init at pins2lts-mc.c:138 frame #8: 0x0000000100001228 pnml2lts-mcmain(argc=1, argv=0x000070000e13dec0) at pins2lts-mc.c:203 frame #9: 0x000000010005febf pnml2lts-mcthread_main(arg=0x0000000101004e58) at hre_pthread.c:195 frame #10: 0x00007fffce7269af libsystem_pthread.dylib_pthread_body + 180 frame #11: 0x00007fffce7268fb libsystem_pthread.dylib_pthread_start + 286 frame #12: 0x00007fffce726101 libsystem_pthread.dylibthread_start + 13

[Meijuh]

@alaarman I have finally fixed the issue (it is on the next branch), you should now be able run the example on OSX. If we are unable to implement spin semantics for edge-based atomic predicates, we should probably disallow spin semantics for edge-based atomic predicates, and remove the "edge-based" code from the spins next-state function in pins2pins-ltl.c.

[alaarman]

I agree, the edge-based semantics are not worked out corrrectly for POR either.

[Meijuh]

So doing action based LTL + POR + any deadlock semantics should be forbidden? That is a separate issue, right?

[Meijuh]

I shall fix the first issue then...

[alaarman]

It might be a separate issue, but it is a reason to remove the edge-based code as you suggested. Its implementation is incomplete wrt POR (at least the invalid combination should be caught and raised as an error).

[Meijuh]

@alaarman regarding the first issue (disabling spin semantics for action-based LTL), do you think it is okay to set the ltsmin semantics by default? These semantics can namely handle both cases (state-based, action-based). If someone wants to enable spin semantics for action-based LTL I can simply raise an error.

[alaarman]

This will break comparisons with SPIN on Promela models (not sure how big of a deal that is). Perhaps we can switch to ltsmin semantics for action-based? Is action-based already well-defined? Otherwise we can set ltsmin semantics as default and raise one warning once a deadlock is found in the LTS (not in the cross-product). This can be done in the LTL layer with a CAS operation.

[Meijuh]

I don't know how well action based LTL (without POR) with ltsmin semantics is implemented? You tell me, at least I have not encountered any issues with it during this years RERS challenge. If there are no deadlocks in the system I guess ltsmin semantics and spin semantics are equivalent no? If that is the case, we could set the semantics to auto, meaning LTSmin will decide for itself (to use ltsmin semantics in case action-based atomic predicates are found.

[alaarman]

Ok, so the earlier issues are only related to POR. In absence of deadlocks the two are indeed equivalent.

[Meijuh]

@alaarman what do you think?

[yanntm]

Hi,

I'm not sure if it is the same issue, but with basic state based predicates I've had some change of behavior causing regression in my test suite recently.

../../lts_install_dir/bin/pins2lts-mc ./gal.so --threads=1 --when --ltl 'X(<>(X([]((LTLAP15==true)))))' --ltl-semantics=textbook

gives a correct answer (finds an accepted counter-example) but both semantics=ltsmin and semantics=spin fail to detect an accepting cycle.

NB : there are no deadlocks in the system. It's an example from MCC. NB2 : I never used the semantics flag before, behavior was fine wrt MCC@PN with default 'spin' semantics in previous tests NB3 : I'm unsure when the regression was introduced (within the last 2 months but that's not very precise). I'm building from next branch.

Trace below, sources attached

rail5.zip

Build an .so with

gcc -c -I/home/ythierry/git/ITS-Tools-pnmcc/lts_install_dir/include -I. -std=c99 -fPIC -O3 model.c
gcc -shared -o gal.so model.o

Traces : textbook is right, the other two are wrong per the MCC results.

[ythierry@oxygen Railroad-PT-005 (master)]$ ../../lts_install_dir/bin/pins2lts-mc  ./gal.so --threads=1 --when --ltl 'X(<>(X([]((LTLAP15==true)))))' --ltl-semantics=textbook
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc, 0.000, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
pins2lts-mc, 0.000: Loading model from ./gal.so
pins2lts-mc, 0.000: library has no initializer
pins2lts-mc, 0.000: loading model GAL
pins2lts-mc, 0.000: completed loading model GAL
pins2lts-mc, 0.000: LTL layer: formula: X(<>(X([]((LTLAP15==true)))))
pins2lts-mc, 0.000: "X(<>(X([]((LTLAP15==true)))))" is not a file, parsing as formula...
pins2lts-mc, 0.000: buchi has 2 states
pins2lts-mc, 0.001: There are 76 state labels and 1 edge labels
pins2lts-mc, 0.001: State length is 55, there are 57 groups
pins2lts-mc, 0.001: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.001: Using a tree table with 2^30 elements
pins2lts-mc, 0.001: Successor permutation: dynamic
pins2lts-mc, 0.001: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014: Accepting cycle FOUND at depth 868!
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014: Explored 909 states 3704 transitions, fanout: 4.075
pins2lts-mc, 0.014: Total exploration time 0.010 sec (0.010 sec minimum, 0.010 sec on average)
pins2lts-mc, 0.014: States per second: 90900, Transitions per second: 370400
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014: State space has 1494 states, 0 are accepting
pins2lts-mc, 0.014: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.014: blue states: 909 (60.84%), transitions: 0 (per worker)
pins2lts-mc, 0.014: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.014: all-red states: 0 (0.00%), bogus 0 (0.00%)
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.014:  
pins2lts-mc, 0.014: Queue width: 8B, total height: 867, memory: 0.01MB
pins2lts-mc, 0.014: Tree memory: 0.0MB, 22.5 B/state, compr.: 10.1%
pins2lts-mc, 0.014: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.014: Stored 56 string chucks using 0MB
pins2lts-mc, 0.014: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.014: Est. total memory use: 0.0MB (~8192.0MB paged-in)

[ythierry@oxygen Railroad-PT-005 (master)]$ ../../lts_install_dir/bin/pins2lts-mc  ./gal.so --threads=1 --when --ltl 'X(<>(X([]((LTLAP15==true)))))' --ltl-semantics=spin
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc, 0.000, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
pins2lts-mc, 0.000: Loading model from ./gal.so
pins2lts-mc, 0.000: library has no initializer
pins2lts-mc, 0.000: loading model GAL
pins2lts-mc, 0.000: completed loading model GAL
pins2lts-mc, 0.000: LTL layer: formula: X(<>(X([]((LTLAP15==true)))))
pins2lts-mc, 0.000: "X(<>(X([]((LTLAP15==true)))))" is not a file, parsing as formula...
pins2lts-mc, 0.000: buchi has 2 states
pins2lts-mc, 0.001: There are 76 state labels and 1 edge labels
pins2lts-mc, 0.001: State length is 55, there are 60 groups
pins2lts-mc, 0.001: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.001: Using a tree table with 2^30 elements
pins2lts-mc, 0.001: Successor permutation: dynamic
pins2lts-mc, 0.001: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc, 0.017: [Blue] 920 levels 1000 states 4060 transitions
pins2lts-mc, 0.027:  
pins2lts-mc, 0.027: Explored 1853 states 7739 transitions, fanout: 4.176
pins2lts-mc, 0.027: Total exploration time 0.020 sec (0.020 sec minimum, 0.020 sec on average)
pins2lts-mc, 0.027: States per second: 92650, Transitions per second: 386950
pins2lts-mc, 0.027:  
pins2lts-mc, 0.027: State space has 1853 states, 0 are accepting
pins2lts-mc, 0.027: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.027: blue states: 1853 (100.00%), transitions: 0 (per worker)
pins2lts-mc, 0.027: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.027: all-red states: 0 (0.00%), bogus 0 (0.00%)
pins2lts-mc, 0.027:  
pins2lts-mc, 0.027: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.027:  
pins2lts-mc, 0.027: Queue width: 8B, total height: 1273, memory: 0.01MB
pins2lts-mc, 0.027: Tree memory: 0.0MB, 21.8 B/state, compr.: 9.8%
pins2lts-mc, 0.027: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.027: Stored 56 string chucks using 0MB
pins2lts-mc, 0.027: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.027: Est. total memory use: 0.0MB (~8192.0MB paged-in)

[ythierry@oxygen Railroad-PT-005 (master)]$ ../../lts_install_dir/bin/pins2lts-mc  ./gal.so --threads=1 --when --ltl 'X(<>(X([]((LTLAP15==true)))))' --ltl-semantics=ltsmin
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc, 0.000, ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
pins2lts-mc, 0.000: Loading model from ./gal.so
pins2lts-mc, 0.000: library has no initializer
pins2lts-mc, 0.000: loading model GAL
pins2lts-mc, 0.000: completed loading model GAL
pins2lts-mc, 0.000: LTL layer: formula: X(<>(X([]((LTLAP15==true)))))
pins2lts-mc, 0.000: "X(<>(X([]((LTLAP15==true)))))" is not a file, parsing as formula...
pins2lts-mc, 0.000: buchi has 2 states
pins2lts-mc, 0.001: There are 76 state labels and 1 edge labels
pins2lts-mc, 0.001: State length is 55, there are 56 groups
pins2lts-mc, 0.001: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.001: Using a tree table with 2^30 elements
pins2lts-mc, 0.001: Successor permutation: dynamic
pins2lts-mc, 0.001: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc, 0.015: [Blue] 961 levels 1000 states 4126 transitions
pins2lts-mc, 0.025:  
pins2lts-mc, 0.025: Explored 1853 states 7739 transitions, fanout: 4.176
pins2lts-mc, 0.025: Total exploration time 0.020 sec (0.020 sec minimum, 0.020 sec on average)
pins2lts-mc, 0.025: States per second: 92650, Transitions per second: 386950
pins2lts-mc, 0.025:  
pins2lts-mc, 0.025: State space has 1853 states, 0 are accepting
pins2lts-mc, 0.025: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.025: blue states: 1853 (100.00%), transitions: 0 (per worker)
pins2lts-mc, 0.025: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.025: all-red states: 0 (0.00%), bogus 0 (0.00%)
pins2lts-mc, 0.025:  
pins2lts-mc, 0.025: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.025:  
pins2lts-mc, 0.025: Queue width: 8B, total height: 1403, memory: 0.01MB
pins2lts-mc, 0.025: Tree memory: 0.0MB, 21.8 B/state, compr.: 9.8%
pins2lts-mc, 0.025: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.025: Stored 56 string chucks using 0MB
pins2lts-mc, 0.025: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.025: Est. total memory use: 0.0MB (~8192.0MB paged-in)

[yanntm]

trying to trace, does'nt this seem suspicious to you ?

patch by Jeroen line 212