Bug in propagation of visibility from state labels to transition groups

[yanntm]

I'm running into issues with --por, that sometimes incorrectly reports empty product when there are solutions. It's a pretty rare issue, that I believe has existed for some time, but I managed to reproduce it on a smallish example.

DatabaseWithMutex-PT-02.zip

So attached source file model.c/model.h, can be compiled with

gcc -shared -o gal.so model.c -I../../lts_install_dir/include/  -fPIC

I then run pins2lts-mc, with or without the final flag --por :

bin/pins2lts-mc ./gal.so --threads=8   --when --ltl '<>(<>((LTLAP9==true)))' --buchi-type=spotba --por

So I've tracked it down to a reproducible bug by changing a single line of the Co-enabled matrix, adding just two entries makes result correct again.

In this case, transition 25 (starting from index 0) cannot be coenabled with transition 0, nor can it be coenabled with transition 26. This is due to existence of an invariant namely

invariant :WaitMutex_1_1 + all_active_1 + Modify_1_1 + WaitMutex_1_2 + Active_1_2 + Active_1_1 + Modify_1_2 = 1

Looking at the .pnml.img.gal gal file or the pnml sources from MCC may help convincing oneself of this fact.

[yanntm]

Here are some traces

With --por, on unmodified model.c generated by my tool (DOES NOT FIND CYCLE):

base) [ythierry@localhost DatabaseWithMutex-PT-02 (master)]$ /home/ythierry/Downloads/v3.0.2/bin/pins2lts-mc ./gal.so --procs=1  --when --ltl '<>(<>((LTLAP9==true)))' --buchi-type=spotba --por
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: Initializing POR dependencies: labels 50, guards 32
pins2lts-mc, 0.000: LTL layer: formula: <>(<>((LTLAP9==true)))
pins2lts-mc, 0.000: "<>(<>((LTLAP9==true)))" is not a file, parsing as formula...
pins2lts-mc, 0.000: Using Spin LTL semantics
pins2lts-mc, 0.004: buchi has 1 states
pins2lts-mc, 0.004: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc, 0.004: Forcing use of the an ignoring proviso (cndfs)
pins2lts-mc, 0.005: There are 52 state labels and 1 edge labels
pins2lts-mc, 0.005: State length is 39, there are 33 groups
pins2lts-mc, 0.005: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.005: Using a tree table with 2^30 elements
pins2lts-mc, 0.005: Successor permutation: dynamic
pins2lts-mc, 0.005: Visible groups: 0 / 33, labels: 1 / 52
pins2lts-mc, 0.005: POR cycle proviso: cndfs (ltl)
pins2lts-mc, 0.005: Global bits: 2, count bits: 2, local bits: 0
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Empty product with LTL!
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Explored 7 states 6 transitions, fanout: 0.857
pins2lts-mc, 0.005: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc, 0.005: States per second: inf, Transitions per second: inf
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: State space has 7 states, 7 are accepting
pins2lts-mc, 0.005: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.005: blue states: 7 (100.00%), transitions: 0 (per worker)
pins2lts-mc, 0.005: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.005: all-red states: 7 (100.00%), bogus 0 (0.00%)
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Queue width: 8B, total height: 3, memory: 0.00MB
pins2lts-mc, 0.005: Tree memory: 0.0MB, 44.6 B/state, compr.: 28.2%
pins2lts-mc, 0.005: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.005: Stored 32 string chucks using 0MB
pins2lts-mc, 0.005: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.005: Est. total memory use: 0.0MB (~8192.0MB paged-in)

Without POR, exactly same thing (DOES FIND cycle)

(base) [ythierry@localhost DatabaseWithMutex-PT-02 (master)]$ /home/ythierry/Downloads/v3.0.2/bin/pins2lts-mc ./gal.so --procs=1  --when --ltl '<>(<>((LTLAP9==true)))' --buchi-type=spotba 
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: <>(<>((LTLAP9==true)))
pins2lts-mc, 0.000: "<>(<>((LTLAP9==true)))" is not a file, parsing as formula...
pins2lts-mc, 0.000: Using Spin LTL semantics
pins2lts-mc, 0.004: buchi has 1 states
pins2lts-mc, 0.004: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc, 0.005: DFS-FIFO for weak LTL, using special progress label 51
pins2lts-mc, 0.005: There are 52 state labels and 1 edge labels
pins2lts-mc, 0.005: State length is 39, there are 33 groups
pins2lts-mc, 0.005: Running dfsfifo using 1 core (sequential)
pins2lts-mc, 0.005: Using a tree table with 2^30 elements
pins2lts-mc, 0.005: Successor permutation: rr
pins2lts-mc, 0.005: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Non-progress cycle FOUND at depth 9!
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Explored 11 states 29 transitions, fanout: 2.636
pins2lts-mc, 0.005: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc, 0.005: States per second: inf, Transitions per second: inf
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Progress states detected: 0
pins2lts-mc, 0.005: Redundant explorations: -56.0000
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Queue width: 8B, total height: 10, memory: 0.00MB
pins2lts-mc, 0.005: Tree memory: 0.0MB, 29.8 B/state, compr.: 18.8%
pins2lts-mc, 0.005: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.005: Stored 32 string chucks using 0MB
pins2lts-mc, 0.005: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.005: Est. total memory use: 0.0MB (~8192.0MB paged-in)

Editing model_mod.c to use original line for transition 25, and default to ones for others. So basically the function at line 438 instead of feeding the real data, feeds line 5, which says everyone enabled, except for transition 25.

(The matrices are stored in sparse form in the C source code to avoid producing source files in megabyte range in some cases. The first value in each "row" is the number of elements in the row, then you have the indexes of non zero entries.)

Bug is revealed, no cycle found

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: Initializing POR dependencies: labels 50, guards 32
pins2lts-mc, 0.000: LTL layer: formula: <>(<>((LTLAP9==true)))
pins2lts-mc, 0.000: "<>(<>((LTLAP9==true)))" is not a file, parsing as formula...
pins2lts-mc, 0.000: Using Spin LTL semantics
pins2lts-mc, 0.004: buchi has 1 states
pins2lts-mc, 0.004: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc, 0.004: Forcing use of the an ignoring proviso (cndfs)
pins2lts-mc, 0.004: There are 52 state labels and 1 edge labels
pins2lts-mc, 0.004: State length is 39, there are 33 groups
pins2lts-mc, 0.004: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.004: Using a tree table with 2^30 elements
pins2lts-mc, 0.005: Successor permutation: dynamic
pins2lts-mc, 0.005: Visible groups: 0 / 33, labels: 1 / 52
pins2lts-mc, 0.005: POR cycle proviso: cndfs (ltl)
pins2lts-mc, 0.005: Global bits: 2, count bits: 2, local bits: 0
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Empty product with LTL!
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Explored 7 states 6 transitions, fanout: 0.857
pins2lts-mc, 0.005: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc, 0.005: States per second: inf, Transitions per second: inf
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: State space has 7 states, 7 are accepting
pins2lts-mc, 0.005: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.005: blue states: 7 (100.00%), transitions: 0 (per worker)
pins2lts-mc, 0.005: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.005: all-red states: 7 (100.00%), bogus 0 (0.00%)
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Queue width: 8B, total height: 3, memory: 0.00MB
pins2lts-mc, 0.005: Tree memory: 0.0MB, 44.6 B/state, compr.: 28.2%
pins2lts-mc, 0.005: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.005: Stored 32 string chucks using 0MB
pins2lts-mc, 0.005: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.005: Est. total memory use: 0.0MB (~8192.0MB paged-in)

Edit/hacked model_mod.c, where still only transition 25 declares a coenabled that is just a bit short (28 coenabled out of 32 possible) and others report everyone else could be coenabled. With respect to previous version, simply added transitions 0 and 26 to the coenabled set (this is incorrect information). Modified lines : around line 426, and the function at line 438, Bug is resorbed, CYCLE FOUND

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: Initializing POR dependencies: labels 50, guards 32
pins2lts-mc, 0.000: LTL layer: formula: <>(<>((LTLAP9==true)))
pins2lts-mc, 0.000: "<>(<>((LTLAP9==true)))" is not a file, parsing as formula...
pins2lts-mc, 0.000: Using Spin LTL semantics
pins2lts-mc, 0.004: buchi has 1 states
pins2lts-mc, 0.004: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc, 0.004: Forcing use of the an ignoring proviso (cndfs)
pins2lts-mc, 0.004: There are 52 state labels and 1 edge labels
pins2lts-mc, 0.004: State length is 39, there are 33 groups
pins2lts-mc, 0.004: Running cndfs using 1 core (sequential)
pins2lts-mc, 0.004: Using a tree table with 2^30 elements
pins2lts-mc, 0.004: Successor permutation: dynamic
pins2lts-mc, 0.004: Visible groups: 0 / 33, labels: 1 / 52
pins2lts-mc, 0.004: POR cycle proviso: cndfs (ltl)
pins2lts-mc, 0.004: Global bits: 2, count bits: 2, local bits: 0
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Accepting cycle FOUND at depth 9!
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Explored 9 states 13 transitions, fanout: 1.444
pins2lts-mc, 0.005: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc, 0.005: States per second: inf, Transitions per second: inf
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: State space has 13 states, 1 are accepting
pins2lts-mc, 0.005: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc, 0.005: blue states: 9 (69.23%), transitions: 0 (per worker)
pins2lts-mc, 0.005: red states: 0 (0.00%), bogus: 0  (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc, 0.005: all-red states: 1 (7.69%), bogus 0 (0.00%)
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Total memory used for local state coloring: 0.0MB
pins2lts-mc, 0.005:  
pins2lts-mc, 0.005: Queue width: 8B, total height: 8, memory: 0.00MB
pins2lts-mc, 0.005: Tree memory: 0.0MB, 40.0 B/state, compr.: 25.3%
pins2lts-mc, 0.005: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.005: Stored 32 string chucks using 0MB
pins2lts-mc, 0.005: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.005: Est. total memory use: 0.0MB (~8192.0MB paged-in)

[yanntm]

My coenabling matrices are computed using an SMT solver combined with Petri net flows computed using the usual incidence matrix, so they are pretty refined (including the fact that transitions such as in this example that have no common support can still be judged not coenable-able).

So I think my model is correct, I could not detect anything with --check --por, and I looked at it by hand to make sure what it reports seems correct (ie. both the invariants and the disablings of potential coenabling that derive from it).

@alaarman Alfons have you met this behavior/ do you have examples with "refined" coenabling matrices ? thanks.

[alaarman]

Thanks for reporting this.

My guess is that there is a bug in the advanced ignoring/visibility proviso implementations. A quick fix seems to be to use --no-V, which switches back to the stronger visibility proviso, which has also effect on the handling of ignoring. This could result in less reduction of course (or better reductions, as its all heuristics anyway in POR).

[yanntm]

Hi,

I'm meeting this issue with some other models, I don't like --no-V, or why did I painstakingly build those matrices in the first place ?

So I'm preparing a patch, basically my feeling is that Visible groups: 0 / 33 is a real issue, other models have the same kind of "oh, let's forget about all transitions" with some visible labels but no visible groups.

My current idea is to attack here : https://github.com/utwente-fmt/ltsmin/blob/master/src/pins-lib/pins-util.c#L116-L122

and add this :

    visible = GBgetPorGroupVisibility(model);
    matrix_t *wr_info = GBgetStateLabelInfo(model);
    if (wr_info) {
        int nvars = dm_ncols (wr_info);
        for (int i = 0; i < nvars; i++) {
            if (dm_is_set(wr_info, index, i)) {
                pins_add_state_variable_visible(model, i);
            }
        }
    }

Looking at the treatment for edge labels, which is doing similar things (propagating), I think this was maybe just an oversight for state labels.

So I'm using the "state label" to "variable" read matrix and basically adding all read variables for this label to observed variables (which impacts observed groups). I kind of would have preferred to use NES/NDS info for this state label if provided by greybox, since that would be more refined than just adding anyone that touches the variable, but this should at least be correct.

Is this the right direction to patch this Alfons ? Also supposing it is, and that we need when adding a state label to observed set to detect which transitions can impact the truth value of the label, am I right in thinking we should use NES/NDS matrices preferably ?

I'll build a PR if it looks OK to you (this is already commited to my fork), once my benchmark/regression suite has finished running with this version, and you've looked at it/approved it.

[alaarman]

@yanntm I see you have another patch to make pins2* thread-safe? bin/pins2lts-mc ./gal.so --threads=8

I need "--procs", but when I force threads it crashes on RTdlopen.

[yanntm]

This was some time ago, I think I mostly configure ltsmin in MThread rather than MProc, and in that mode there was some issue with options parsing, so we added a small barrier around that. But that has been merged I believe, it's this commit https://github.com/utwente-fmt/ltsmin/commit/5ad6af84a2a2236d995828f64fde2ab6cef5effb

BUT it seems I went for some pthread mutex hack; maybe a HRE_barrier would be better so it also works in MProc, if this is the same bug you're running into.

https://github.com/utwente-fmt/ltsmin/issues/181 says it's diagnosed on MT; but I only ever tried MT so maybe bug occurs in MP context too.

[yanntm]

see also these comments when these patches were adopted (by you :D) https://github.com/utwente-fmt/ltsmin/pull/182

[alaarman]

hehe :) I neglected to use the latest branch... thanks for pointing that out.

[yanntm]

happy I could help; I feel pretty happy about being able to help you with ltsmin in this instance :D cheers

[alaarman]

The bug was in the enforcement of the provisos. See 730248c. Your patch worked by accident, because you overwrote the visible variable. But the idea was sound.

[yanntm]

Awesome ! Thanks a lot, I can remove that --no-v and my propagate to groups patch, you're right that your patch seems much much better, just a silly little bug apparently, thanks again for taking the time to diagnose and patch it. I'll rerun my benchmark maybe with some more runs passing with these weaker constraints on the POR. I had noticed that --no-V did have measurable impact on number of solved instances (i.e. yes all results were now correct, but some runs now timeout).

[alaarman]

Great, thanks for confirming that, @yanntm. Well actually it was not so minor. Apparently, introduced the bug when adding the transaction reduction algorithms...