Then we are testing a formula in TGBA vs SPOTBA modes !(G(((F(p0) U G(p1))||F(p2)||(p3 U (p4||G(p3)))))) in spot syntax
Note that according to Spot, this property is : "Hierarchy of Manna and Pnueli This formula describes a reactivity property." and "Safety-Liveness classification This formula represents a liveness property."
So pretty much the max complexity.
We also know that this property is false from other tools as this is an MCC example, so the product should be non empty.
So to feed this to LTSmin, we try :
pins2lts-mc './gal.so' '--threads=1' '--ltl' '[](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))' '--buchi-type=tgba'
So, minimal flags, threads=1 to avoid any interleaving issues, no POR.
Unfortunately this returns True (exit value 0), the product is empty. If we switch to --buchi-type=spotba LTSmin correctly finds an accepted run.
A full trace :
[ythierry@oxygen ltsmin2011502938770432776]$ ~/git/ltsminYannTM/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=1' '--ltl' '[](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))' '--buchi-type=tgba' ; echo $?
pins2lts-mc: Registering PINS so language module
pins2lts-mc: Loading model from ./gal.so
pins2lts-mc: library has no initializer
pins2lts-mc: loading model GAL
pins2lts-mc: completed loading model GAL
pins2lts-mc: LTL layer: formula: [](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))
pins2lts-mc: "[](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))" is not a file, parsing as formula...
pins2lts-mc: Using Spin LTL semantics
pins2lts-mc: buchi has 4 states
pins2lts-mc: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc: DFS-FIFO for weak LTL, using special progress label 32
pins2lts-mc: There are 33 state labels and 2 edge labels
pins2lts-mc: State length is 21, there are 36 groups
pins2lts-mc: Running dfsfifo using 1 core (sequential)
pins2lts-mc: Using a tree table with 2^27 elements
pins2lts-mc: Successor permutation: rr
pins2lts-mc: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc: 1 levels 1000 states 7251 transitions
pins2lts-mc: 1 levels 2000 states 14510 transitions
pins2lts-mc:
pins2lts-mc:
pins2lts-mc: Explored 2598 states 17126 transitions, fanout: 6.592
pins2lts-mc: Total exploration time 0.020 sec (0.020 sec minimum, 0.020 sec on average)
pins2lts-mc: States per second: 129900, Transitions per second: 856300
pins2lts-mc:
pins2lts-mc: Progress states detected: 2597
pins2lts-mc: Redundant explorations: 0.0000
pins2lts-mc:
pins2lts-mc: Queue width: 8B, total height: 676, memory: 0.01MB
pins2lts-mc: Tree memory: 0.0MB, 10.6 B/state, compr.: 12.4%
pins2lts-mc: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc: Stored 26 string chucks using 0MB
pins2lts-mc: Total memory used for chunk indexing: 0MB
pins2lts-mc: Est. total memory use: 0.0MB (~1024.0MB paged-in)
0
[ythierry@oxygen ltsmin2011502938770432776]$ ~/git/ltsminYannTM/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=1' '--ltl' '[](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))' '--buchi-type=spotba' ; echo $?
pins2lts-mc: Registering PINS so language module
pins2lts-mc: Loading model from ./gal.so
pins2lts-mc: library has no initializer
pins2lts-mc: loading model GAL
pins2lts-mc: completed loading model GAL
pins2lts-mc: LTL layer: formula: [](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))
pins2lts-mc: "[](((<>((LTLAPp0==true)) U []((LTLAPp1==true)))||<>((LTLAPp2==true))||((LTLAPp3==true) U ((LTLAPp4==true)||[]((LTLAPp3==true))))))" is not a file, parsing as formula...
pins2lts-mc: Using Spin LTL semantics
pins2lts-mc: buchi has 5 states
pins2lts-mc: There are 32 state labels and 1 edge labels
pins2lts-mc: State length is 21, there are 39 groups
pins2lts-mc: Running cndfs using 1 core (sequential)
pins2lts-mc: Using a tree table with 2^27 elements
pins2lts-mc: Successor permutation: dynamic
pins2lts-mc: Global bits: 2, count bits: 0, local bits: 0
pins2lts-mc:
pins2lts-mc: Accepting cycle FOUND at depth 721!
pins2lts-mc:
pins2lts-mc:
pins2lts-mc: Explored 942 states 5834 transitions, fanout: 6.193
pins2lts-mc: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc: States per second: inf, Transitions per second: inf
pins2lts-mc:
pins2lts-mc: State space has 1219 states, 161 are accepting
pins2lts-mc: cndfs_1 (permutation: dynamic) stats:
pins2lts-mc: blue states: 942 (77.28%), transitions: 0 (per worker)
pins2lts-mc: red states: 0 (0.00%), bogus: 0 (0.00%), transitions: 0, waits: 0 (0.00 sec)
pins2lts-mc: all-red states: 161 (13.21%), bogus 0 (0.00%)
pins2lts-mc:
pins2lts-mc: Total memory used for local state coloring: 0.0MB
pins2lts-mc:
pins2lts-mc: Queue width: 8B, total height: 721, memory: 0.01MB
pins2lts-mc: Tree memory: 0.0MB, 11.6 B/state, compr.: 13.5%
pins2lts-mc: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc: Stored 26 string chucks using 0MB
pins2lts-mc: Total memory used for chunk indexing: 0MB
pins2lts-mc: Est. total memory use: 0.0MB (~1024.0MB paged-in)
1
So, very suspicious to me is the report of
pins2lts-mc: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc: DFS-FIFO for weak LTL, using special progress label 32
in TGBA mode, as discussed in the introduction, this is not a weak formula at all.
Hi,
So I have found what seems to be a bug in TGBA mode.
Attached model is a Petri net encoded in PINS, pretty much the smallest I could isolate. model.zip
compile with (??? stands for LTSmin install folder)
Then we are testing a formula in TGBA vs SPOTBA modes
!(G(((F(p0) U G(p1))||F(p2)||(p3 U (p4||G(p3))))))in spot syntaxNote that according to Spot, this property is : "Hierarchy of Manna and Pnueli This formula describes a reactivity property." and "Safety-Liveness classification This formula represents a liveness property."
So pretty much the max complexity.
We also know that this property is false from other tools as this is an MCC example, so the product should be non empty.
So to feed this to LTSmin, we try :
So, minimal flags, threads=1 to avoid any interleaving issues, no POR.
Unfortunately this returns True (exit value 0), the product is empty. If we switch to
--buchi-type=spotbaLTSmin correctly finds an accepted run.A full trace :
So, very suspicious to me is the report of
in TGBA mode, as discussed in the introduction, this is not a weak formula at all.
So perhaps some issue with the way we test for weakness in a TGBA around here : https://github.com/utwente-fmt/ltsmin/blob/fea250ecc03ac456f26e272f44b8035eae968b9f/src/pins-lib/pins2pins-ltl.c#L779-L793
A simple workaround is to avoid using TGBA and use spotba instead.