ICC Experiments using REFINER

The experiment files can be obtained via this link (when using Safari, open in New Window or Tab).

The ICC experiments have been conducted by running refiner -icc -n [networkname] from the command-line, where [networkname] is the following, launched from the corresponding folder:
  • 1394: 1394property
  • 1394: 1394property1
  • transit: transitproperty
  • waferstepper: waferstepperproperty
  • des: desproperty
  • cfs: cfsproperty
  • lamport: lamportproperty
  • lann5: lann5property
  • lann6: lann6property
  • lann7: lann7property
  • havi: haviproperty
  • peterson: petersonproperty
  • szymanski: szymanskiproperty

Comparative experiments

Other experiments that can be conducted with the experiment files above, are partial model checking experiments. These can be run using the CADP toolbox. For this purpose, please install CADP, and launch the svl tool from the command-line, providing the buildsystem.svl file present in each experiment folder as an argument.

Besides this, also the multi-core explicit-state model checking tool of the LTSmin toolset can be run to on-the-fly check for property violations. However, in order to make this work, the, still experimental, support for EXP files must be added. This is currently not yet part of the publicly available version of LTSmin.