Error diagnostic: nbac2lucky and lucky

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.)

NBAC2LUCKY Reference Manual

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

Bertrand Jeannet, February 10, 2011

Error diagnostic: nbac2lucky and lucky