Closed yanntm closed 1 year ago
Hi,
While this does patch an issue with the traces, I get incomplete transition labels as when I set more than one thread, so there will be probably a follow up patch to ensure traces are correct and complete in a MT context.
I haven't realy diagnosed this issue yet, it's the first time I try to use LTSMin traces in a CEGAR context, where I exploit them automatically. I'm using e.g. ltsmin-printtrace trace.gcf trace.csv
to interpret, but for my use case I'd rather pass --trace trace.csv
to the original invocation, so I might add support for that scenario (recognize extension csv when asked for a trace) in the main tool if that sounds reasonable.
Are there any examples you know of that use LTSmin traces in a tool using LTL part of LTSMin ?
The gcf seems incomplete in a MT (threads>1) context most of the time.
thanks
yann
A direct --trace trace.csv
(bypassing gcf) makes sense to me, at least from a user perspective. The gcf variant could still make sense for compressing large traces (long or with large states).
And thanks for the contribution of the patch!
We were missing one label when looking at LTL traces, because there are as many states as transitions (with the lasso).
e.g. before : more trace.csv 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,po s2_RIGHT:int,pos2_LOOK:int,pos2_TOTAL:int,pos3_MOVE:int,pos3_STAY:int,pos3_LEFT:int,pos3_RIGHT:int,pos3_LOOK:int,pos3_TOTAL:int,LTLAPtower:boolean,buchi_accept:LTL_bool,weak_ltl_progress:LTL_bool,action:action 0,0,0,0,0,3,3,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_LOOK" 0,1,0,0,0,2,3,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_MOVE" 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,"tr3_LOOK" 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,false,true,false, 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,"tr3_LOOK"
After : 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,po s2_RIGHT:int,pos2_LOOK:int,pos2_TOTAL:int,pos3_MOVE:int,pos3_STAY:int,pos3_LEFT:int,pos3_RIGHT:int,pos3_LOOK:int,pos3_TOTAL:int,LTLAPtower:boolean,buchi_accept:LTL_bool,weak_ltl_progress:LTL_bool,action:action 0,0,0,0,0,3,3,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_LOOK" 0,1,0,0,0,2,3,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,false,true,false,"tr0_MOVE" 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,"tr3_LOOK" 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,1,false,true,false,"tr3_STAY" 0,0,0,0,0,2,2,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,false,true,false,"tr3_LOOK"