|
| | | Error diagnostic: nbac2lucky and lucky |
We presented an efficient method [5] to generate counter-examples to a property that NBac cannot prove. The implementation is integrated in the Ludic debugger.
It is also available directly from NBac, by connecting directly to it the Lucky sequence generator and the Lulu simulator. (See here for the main tools around Lustre.)
The nbac2lucky tool allow to convert a NBAC file with an explicit control structure to the lucky format.
Usage: nbac2lucky <list of options> <filename> -comp <str> : using decomposition for putting weights ? none: no (default) cfc: strongly connected components scfc: strongly connected sub-components -comp_factor <n> : component factor (default 10) -path_factor <n> : path factor (default 2) -o <filename> : Output Lucky automaton file -help display this list of options --help display this list of options
|
| | | Error diagnostic: nbac2lucky and lucky |