search

utwente-fmt / ltsmin

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

Issues with LTL traces in MT context #209

Open yanntm opened 1 year ago

yanntm commented 1 year ago

Hi, So I'm trying to get traces out of ltl, but the results are a bit random, and the files tend to be broken.

Attached model, when run with 8 threads, typically produces a gcf file with incomplete or completely wrong information, or even a corrupt gcf that subsequently crashes ltsmin-printtrace. In particular resolution of edge labels seems bad, the states themselves are consistent.

I think the problem comes from this invocation : https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/dfs-fifo.c#L104

We are coming from here : https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/dfs-fifo.c#L123-L127 Where we did set LTSMIN exit to signal but the barrier is not strong to ensure only one thread is still working.

Most other invocations to trace are much more heavily protected or delayed as in this instance : https://github.com/utwente-fmt/ltsmin/blob/master/src/pins2lts-mc/algorithm/ltl.c#L77-L89

The call that was commented + the comment preceding it makes me think the issue has been met before. @alaarman Could we use the same kind of behavior for NonProgress cycles ? somehow print the trace with a single thread AFTER all threads have acknowledged the EXIT sign.

In other cases, there is also care taken, e.g. only master is working here https://github.com/utwente-fmt/ltsmin/blob/3499bb5afb06c5e955d0df5bb3220eb7b654f3da/src/pins2lts-mc/algorithm/ufscc.c#L725

Attached are a few test files example.zip

Compile with 'gcc' -g '-c' '-I/home/ythierry/git/ITSTools/ltsmin/fr.lip6.move.gal.ltsmin.binaries/bin/include/' '-I.' '-std=c99' '-fPIC' '-O0' 'model.c';'gcc' -g '-c' '-I/home/ythierry/git/ITSTools/ltsmin/fr.lip6.move.gal.ltsmin.binaries/bin/include/' '-I.' '-std=c99' '-fPIC' '-O0' 'strat.c';'gcc' -g '-shared' '-o' 'gal.so' 'model.o' strat.o

Then I'm running this: /home/ythierry/git/LTSmin-BinaryBuilds/ltsmin/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=1' '--when' '--ltl' '<>((LTLAPtower==true))' '--buchi-type=spotba' '-v' '--trace' 'trace.gcf'

So threads=1 works, threads=8 is mostly producing corrupt GCF file.

**

thanks for your insight, I'll keep investigating, but it's one of those subtle concurrency issues so not easy to fully diagnose, and I have the feeling that the solution has already been developed, just this call was not updated to honor it.

yanntm commented 1 year ago

Here is a trace showing the issues :

[ythierry@oxygen gperf14242588368054502952]$ /home/ythierry/git/LTSmin-BinaryBuilds/ltsmin/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=1' '--when' '--ltl' '<>((LTLAPtower==true))' '--buchi-type=spotba' '-v' '--trace' 'trace.gcf' 
pins2lts-mc, 0.000: LTL semantics: none
pins2lts-mc, 0.000: Buchi type: spotba
pins2lts-mc, 0.000: Registering PINS so language module
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: <>((LTLAPtower==true))
pins2lts-mc, 0.000: "<>((LTLAPtower==true))" is not a file, parsing as formula...
pins2lts-mc, 0.000: success!
pins2lts-mc, 0.000: Using Spin LTL semantics
pins2lts-mc, 0.000: Spot LTL formula:  ! ( <> ("(LTLAPtower ==  true )"))
pins2lts-mc, 0.004: buchi has 1 states
pins2lts-mc, 0.004:  state 0: accepting
pins2lts-mc, 0.004:   -> 0, | !(LTLAPtower ==  true )
pins2lts-mc, 0.004: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc, 0.006: DFS-FIFO for weak LTL, using special progress label 2
pins2lts-mc, 0.006: There are 3 state labels and 1 edge labels
pins2lts-mc, 0.006: State length is 19, there are 16 groups
pins2lts-mc, 0.006: Running dfsfifo using 1 core (sequential)
pins2lts-mc, 0.006: Using a tree table with 2^26 elements
pins2lts-mc, 0.006: Successor permutation: rr
pins2lts-mc, 0.006: Global bits: 2, count bits: 0, local bits: 0
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,0,0,0,1,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0, NEXT : pos=1 A=LOOK 0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0, NEXT : pos=1 A=STAY 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
pins2lts-mc, 0.006:  
pins2lts-mc, 0.006: Non-progress cycle FOUND at depth 4!
pins2lts-mc, 0.006:  
pins2lts-mc, 0.006: reconstructed trace length: 3
pins2lts-mc, 0.006: constructing the trace took 0.000 real 0.000 user 0.000 sys
pins2lts-mc, 0.006: 52385211    (1),
pins2lts-mc, 0.006: 27783289    (2),
pins2lts-mc, 0.006: 64994584    (3),
pins2lts-mc, 0.006: 26105137    (4),
pins2lts-mc, 0.006: 64994584    (5),
pins2lts-mc, 0.006: Writing trace to trace.gcf
pins2lts-mc, 0.007: finding edge for state 0
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
pins2lts-mc, 0.007: finding edge for state 1
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
pins2lts-mc, 0.007: finding edge for state 2
0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,0,0,0,1,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0, NEXT : pos=1 A=LOOK 0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0,
pins2lts-mc, 0.007: finding edge for state 3
0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,1,0,0,0,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0, NEXT : pos=1 A=STAY 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
pins2lts-mc, 0.007: comment is archive I/O (trace.gcf)
pins2lts-mc, 0.007: LTS has 1 initial state(s) (trace.gcf)
pins2lts-mc, 0.007: segment 0 has 4 states (trace.gcf)
pins2lts-mc, 0.007: segment 0 has 4 transitions (trace.gcf)
pins2lts-mc, 0.007: accounted for 4 states and 4 transitions (trace.gcf)
pins2lts-mc, 0.007:  worker ran 0.000 sec
pins2lts-mc, 0.007: 4 levels 4 states 8 transitions
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Explored 4 states 8 transitions, fanout: 2.000
pins2lts-mc, 0.007: Total exploration time 0.000 sec (0.000 sec minimum, 0.000 sec on average)
pins2lts-mc, 0.007: States per second: inf, Transitions per second: inf
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Load balancer:
pins2lts-mc, 0.007: Splits: 0
pins2lts-mc, 0.007: Load transfer: 0
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Progress states detected: 0
pins2lts-mc, 0.007: Redundant explorations: -50.0000
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Queue width: 8B, total height: 5, memory: 0.00MB
pins2lts-mc, 0.007: Tree memory: 0.0MB, 40.0 B/state, compr.: 51.3%
pins2lts-mc, 0.007: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc, 0.007: Stored 15 string chucks using 0MB
pins2lts-mc, 0.007: String table 'int': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc, 0.007: String table 'action': 0MB pointers, 0MB tables (1706.67% overhead), 15 strings (distr.: 0.00)
pins2lts-mc, 0.007: String table 'boolean': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc, 0.007: String table 'buchi': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc, 0.007: String table 'LTL_bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc, 0.007: Total memory used for chunk indexing: 0MB
pins2lts-mc, 0.007: Est. total memory use: 0.0MB (~512.0MB paged-in)
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Database statistics:
pins2lts-mc, 0.007: Elements: 8
pins2lts-mc, 0.007: Nodes: 40
pins2lts-mc, 0.007: Misses: 0
pins2lts-mc, 0.007: Tests: 0
pins2lts-mc, 0.007: Rehashes: 0
pins2lts-mc, 0.007:  
pins2lts-mc, 0.007: Memory usage statistics:
pins2lts-mc, 0.007: Queue: 0.0 MB
pins2lts-mc, 0.007: DB: 0.0 MB
pins2lts-mc, 0.007: Colors: 0.0 MB
pins2lts-mc, 0.007: Chunks: 0.0 MB
pins2lts-mc, 0.007: DB paged in: 512.0 MB
[ythierry@oxygen gperf14242588368054502952]$ ~/git/LTSmin-BinaryBuilds/ltsmin/src/ltsmin-printtrace/ltsmin-printtrace trace.gcf trace.csv ; more trace.csvltsmin-printtrace: Writing output to 'trace.csv'
ltsmin-printtrace: realloc
ltsmin-printtrace: action labeled, detecting silent step
ltsmin-printtrace: no silent label
ltsmin-printtrace: length of trace is 4
ltl:buchi,pos0_MOVE:int,pos0_STAY:int,pos0_LEFT:int,pos0_RIGHT:int,pos0_LOOK:int,pos0_TOTAL:int,pos1_MOVE:int,pos1_STAY:int,pos1_LEFT:int,pos1_RIGHT:int,pos1_LOOK:int,pos1_TOTAL:int,pos2_MOVE:int,pos2_STAY:int,pos2_LEFT:int,pos2_R
IGHT:int,pos2_LOOK:int,pos2_TOTAL:int,LTLAPtower:boolean,buchi_accept:LTL_bool,weak_ltl_progress:LTL_bool,action:action
0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_LOOK"
0,1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_MOVE"
0,0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,false,true,false,"tr1_LOOK"
0,0,0,0,0,1,1,0,1,0,0,0,1,0,0,0,0,0,0,false,true,false,"tr1_STAY"
0,0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,false,true,false,"tr1_LOOK"
[ythierry@oxygen gperf14242588368054502952]$

So with one thread it seems good, 8 thread is not. Also note we went into the NONPROGRESS CYCLE case.

yanntm commented 1 year ago

A trace for 8 threads : incorrect file produced

[ythierry@oxygen gperf14242588368054502952]$ /home/ythierry/git/LTSmin-BinaryBuilds/ltsmin/src/pins2lts-mc/pins2lts-mc './gal.so' '--threads=8' '--when' '--ltl' '<>((LTLAPtower==true))' '--buchi-type=spotba' '-v' '--trace' 'trace.gcf' 
pins2lts-mc, 0.000: LTL semantics: none
pins2lts-mc, 0.000: Buchi type: spotba
pins2lts-mc, 0.000: Registering PINS so language module
pins2lts-mc( 0/ 8), 0.000: Loading model from ./gal.so
pins2lts-mc( 1/ 8), 0.000: library has no initializer
pins2lts-mc( 1/ 8), 0.000: loading model GAL
pins2lts-mc( 2/ 8), 0.000: library has no initializer
pins2lts-mc( 3/ 8), 0.000: library has no initializer
pins2lts-mc( 0/ 8), 0.000: library has no initializer
pins2lts-mc( 3/ 8), 0.000: loading model GAL
pins2lts-mc( 5/ 8), 0.000: library has no initializer
pins2lts-mc( 6/ 8), 0.000: library has no initializer
pins2lts-mc( 0/ 8), 0.000: loading model GAL
pins2lts-mc( 2/ 8), 0.000: loading model GAL
pins2lts-mc( 7/ 8), 0.000: library has no initializer
pins2lts-mc( 7/ 8), 0.000: loading model GAL
pins2lts-mc( 4/ 8), 0.000: library has no initializer
pins2lts-mc( 4/ 8), 0.000: loading model GAL
pins2lts-mc( 6/ 8), 0.000: loading model GAL
pins2lts-mc( 4/ 8), 0.000: completed loading model GAL
pins2lts-mc( 6/ 8), 0.000: completed loading model GAL
pins2lts-mc( 4/ 8), 0.000: LTL layer: formula: <>((LTLAPtower==true))
pins2lts-mc( 0/ 8), 0.000: completed loading model GAL
pins2lts-mc( 3/ 8), 0.000: completed loading model GAL
pins2lts-mc( 1/ 8), 0.000: completed loading model GAL
pins2lts-mc( 2/ 8), 0.000: completed loading model GAL
pins2lts-mc( 5/ 8), 0.000: loading model GAL
pins2lts-mc( 7/ 8), 0.000: completed loading model GAL
pins2lts-mc( 4/ 8), 0.000: "<>((LTLAPtower==true))" is not a file, parsing as formula...
pins2lts-mc( 5/ 8), 0.000: completed loading model GAL
pins2lts-mc( 4/ 8), 0.000: Using Spin LTL semantics
pins2lts-mc( 4/ 8), 0.000: Spot LTL formula:  ! ( <> ("(LTLAPtower ==  true )"))
pins2lts-mc( 0/ 8), 0.005: Weak Buchi automaton detected, adding non-accepting as progress label.
pins2lts-mc( 0/ 8), 0.056: DFS-FIFO for weak LTL, using special progress label 2
pins2lts-mc( 0/ 8), 0.056: There are 3 state labels and 1 edge labels
pins2lts-mc( 0/ 8), 0.056: State length is 19, there are 16 groups
pins2lts-mc( 0/ 8), 0.056: Running dfsfifo using 8 cores
pins2lts-mc( 0/ 8), 0.056: Using a tree table with 2^26 elements
pins2lts-mc( 0/ 8), 0.056: Successor permutation: rr
pins2lts-mc( 0/ 8), 0.056: Global bits: 2, count bits: 0, local bits: 0
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,
2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 1,0,0,0,0,1,0,0,0,0,1,1,0,0,0,0,0,0,
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,0,0,0,1,1,0,0,0,0,0,0,0,1,0,0,0,1,
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,0,0,0,1,1,0,0,0,0,0,0,0,1,0,0,0,1,
1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=MOVE 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,2,
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=STAY 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=STAY 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,
1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=MOVE 0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,1,1,
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,
pins2lts-mc( 6/ 8), 0.056:  
pins2lts-mc( 6/ 8), 0.056: Non-progress cycle FOUND at depth 4!
1,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 1,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,
pins2lts-mc( 6/ 8), 0.056:  
pins2lts-mc( 6/ 8), 0.056: reconstructed trace length: 3
pins2lts-mc( 6/ 8), 0.056: constructing the trace took 0.000 real 0.000 user 0.000 sys
pins2lts-mc( 6/ 8), 0.056: 52385211     (1),
pins2lts-mc( 6/ 8), 0.056: 27783289     (2),
pins2lts-mc( 6/ 8), 0.056: 12151825     (3),
pins2lts-mc( 6/ 8), 0.056: 22083083     (4),
pins2lts-mc( 6/ 8), 0.056: 12151825     (5),
pins2lts-mc( 6/ 8), 0.056: Writing trace to trace.gcf
pins2lts-mc( 6/ 8), 0.057: finding edge for state 0
0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,
pins2lts-mc( 6/ 8), 0.057: finding edge for state 1
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=MOVE 0,0,0,0,1,1,0,0,0,0,1,1,0,0,0,0,0,0,
1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0, NEXT : pos=0 A=LOOK 2,0,0,0,0,2,0,0,0,0,0,0,0,0,0,0,0,0,
pins2lts-mc( 6/ 8), 0.057: finding edge for state 2
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,0,0,0,1,1,0,0,0,0,0,0,0,1,0,0,0,1,
pins2lts-mc( 6/ 8), 0.057: finding edge for state 3
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=0 A=STAY 0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,
0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1, NEXT : pos=2 A=LOOK 0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,1,
pins2lts-mc( 6/ 8), 0.057: comment is archive I/O (trace.gcf)
pins2lts-mc( 6/ 8), 0.057: LTS has 1 initial state(s) (trace.gcf)
pins2lts-mc( 6/ 8), 0.057: segment 0 has 4 states (trace.gcf)
pins2lts-mc( 6/ 8), 0.057: segment 0 has 4 transitions (trace.gcf)
pins2lts-mc( 6/ 8), 0.057: accounted for 4 states and 4 transitions (trace.gcf)
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: mean standard work distribution: 129.1% (states) 129.4% (transitions)
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Explored 12 states 25 transitions, fanout: 2.083
pins2lts-mc( 0/ 8), 0.058: Total exploration time 0.010 sec (0.000 sec minimum, 0.001 sec on average)
pins2lts-mc( 0/ 8), 0.058: States per second: 1200, Transitions per second: 2500
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Load balancer:
pins2lts-mc( 0/ 8), 0.058: Splits: 0
pins2lts-mc( 0/ 8), 0.058: Load transfer: 0
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Progress states detected: 0
pins2lts-mc( 0/ 8), 0.058: Redundant explorations: -7.6923
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Queue width: 8B, total height: 15, memory: 0.00MB
pins2lts-mc( 0/ 8), 0.058: Tree memory: 0.0MB, 30.2 B/state, compr.: 38.7%
pins2lts-mc( 0/ 8), 0.058: Tree fill ratio (roots/leafs): 0.0%/0.0%
pins2lts-mc( 0/ 8), 0.058: Stored 28 string chucks using 0MB
pins2lts-mc( 0/ 8), 0.058: String table 'int': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc( 0/ 8), 0.058: String table 'action': 0MB pointers, 0MB tables (1706.67% overhead), 15 strings (distr.: 3.69)
pins2lts-mc( 0/ 8), 0.058: String table 'boolean': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc( 0/ 8), 0.058: String table 'buchi': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc( 0/ 8), 0.058: String table 'LTL_bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
pins2lts-mc( 0/ 8), 0.058: Total memory used for chunk indexing: 0MB
pins2lts-mc( 0/ 8), 0.058: Est. total memory use: 0.0MB (~512.0MB paged-in)
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Database statistics:
pins2lts-mc( 0/ 8), 0.058: Elements: 13
pins2lts-mc( 0/ 8), 0.058: Nodes: 49
pins2lts-mc( 0/ 8), 0.058: Misses: 0
pins2lts-mc( 0/ 8), 0.058: Tests: 0
pins2lts-mc( 0/ 8), 0.058: Rehashes: 0
pins2lts-mc( 0/ 8), 0.058:  
pins2lts-mc( 0/ 8), 0.058: Memory usage statistics:
pins2lts-mc( 0/ 8), 0.058: Queue: 0.0 MB
pins2lts-mc( 0/ 8), 0.058: DB: 0.0 MB
pins2lts-mc( 0/ 8), 0.058: Colors: 0.0 MB
pins2lts-mc( 0/ 8), 0.058: Chunks: 0.0 MB
pins2lts-mc( 0/ 8), 0.058: DB paged in: 512.0 MB
[ythierry@oxygen gperf14242588368054502952]$ ~/git/LTSmin-BinaryBuilds/ltsmin/src/ltsmin-printtrace/ltsmin-printtrace trace.gcf trace.csv ; more trace.csvltsmin-printtrace: Writing output to 'trace.csv'
ltsmin-printtrace: realloc
ltsmin-printtrace: action labeled, detecting silent step
ltsmin-printtrace: no silent label
ltsmin-printtrace: length of trace is 4
ltl:buchi,pos0_MOVE:int,pos0_STAY:int,pos0_LEFT:int,pos0_RIGHT:int,pos0_LOOK:int,pos0_TOTAL:int,pos1_MOVE:int,pos1_STAY:int,pos1_LEFT:int,pos1_RIGHT:int,pos1_LOOK:int,pos1_TOTAL:int,pos2_MOVE:int,pos2_STAY:int,pos2_LEFT:int,pos2_R
IGHT:int,pos2_LOOK:int,pos2_TOTAL:int,LTLAPtower:boolean,buchi_accept:LTL_bool,weak_ltl_progress:LTL_bool,action:action
0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,""
0,1,0,0,0,1,2,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_STAY"
0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,""
0,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,""
0,0,0,0,0,1,1,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,""
[ythierry@oxygen gperf14242588368054502952]$
yanntm commented 1 year ago

Ok so some follow up examples, this one produces a GCF that ltsmin-printtrace will crash on.

It's as small as I could make it, we have a lasso in 2 states : initial -> s1 -> initial And no prefix.

Unfortunately, the code in here : https://github.com/utwente-fmt/ltsmin/blob/master/src/pins2lts-mc/algorithm/dfs-fifo.c#L63-L105

Is incorrectly building a trace with 4 elements instead of just 2.

I'm starting to use "-ufscc" to bypass this dfs-fifo code.

So there is a more general issue with the traces I think, I tried all search strategies, this is what I obtain :

Here are current results (SINGLE THREAD)

The results are more bleak with 8 threads :

So, I'm using ufscc as search strategy for now. Attached are reproduction files (same compilation as in the first message of the thread). There are also logs of running with the various strategies. exampleSmall.zip

yanntm commented 1 year ago

Hi, just to say there is no immediate urgency or deadline, my workaround threads=1 and ufscc work fine the issue is to keep a trace of this issue and what I could diagnose. The example provided is very small (a few states) so is meant to help debug. I was still very happy to have LTSmin in this scenario my transition relation is really tricky so coding it in C was the most relevant path, and LTSmin is the tool for this. I'm going to add nice symmetries embedded in the transition relation, so I'll lose my dependency matrices (reordering with my symmetries might shift all state variables, so my read/write will be dense), and probably POR can't help me because of that, but overall it's a really nice use case of LTSmin to use custom transition relation in a CEGAR loop, and it works well. I'll spend some more time on the issue in Sept, but the results are good enough for now so no rush. I'm sorry probably the first posts are mis-diagnosing, the issue seems more deeply embedded than I first thought as the later post indicates.

jacopol commented 1 year ago

Hi, thanks for using (single threaded) and thanks for reporting the issues (mainly in multi-threaded). Let me share some of the history of gcf: It has been developed early on in LTSmin, when it was mainly a distributed tool for state space generation (running over MPI). It solves the issue that multiple nodes in a network write streams of states to disk, in the old times where the OS was not good at "disk striping".

Meanwhile, LTSmin has grown quite a bit, supporting multiple action labels and state labels, and creating multi-core computations. Also, it was decided to reuse the gcf-format also for storing traces (since they are a special form of state spaces). I'm afraid the gcf-support is somewhat lacking behind on these newer developments. And - as you demonstrated - several combinations of use-cases with gcf are not properly tested.

Any contributions on these are much appreciated.