INCLUDER (tracer)

Trace Inclusion for Data Word Automata

Related Publications:

  1. R. Iosif, A. Rogalewicz, T. Vojnar: Abstraction Refinement for Trace Inclusion of Infinite State Systems PDF (accepted to TACAS'16).

1. Requirements

  1. MathSat solver.
  2. C++ compiler supporting the standard C++ 2011 (tested with g++ (GCC) 5.1.1).

2. License, Download, Instalation

License GNU GPL v3 or any later, see http://www.gnu.org/licenses/gpl.html for more details.

3. Examples

The archive contains a set of examples derived from several sources [2], [3], [4], [5], [6], [7]. See our paper [1] for more details.

Network A consists of a single component

ExampleFilenameResults
Simple 1 simple-examples/example-simple1.ccex.
Simple 2 simple-examples/example-simple2.c ok
Simple 3 simple-examples/example-simple3.c ok
Arrays shift arrays/example-array-shifting.c ok
Array simple arrays/filip-simple.cok
Array rotation 1arrays/array-rotation-radu.c ok
Array rotation 2arrays/filip-rotation.c ok
Array splitarrays/filip-split.c ok
Train (nonparametric version)timed-automata/example-rr-crossing.c ok
HW counter 1hw-examples/example-simple-hw-counter.cok
HW counter 2hw-examples/example-hw-counter.c ok
Synchronous LIFOhw-examples/ales-synlifo.c ok
ABP-error protocols/example-abp-error.ccex.
ABP-correct protocols/example-abp-correct.c ok
Producer-consumer (nonparametric version)protocols/example-producer-consumer.cok

Network A has two and more components

Open the corresponding file and adjust the parameters in its header. The recompile the example.
ExampleFilenameResultsAdjustable Parameters
Running running/running.cok N (the number of processes)
Train Open-Kronos/Train/train-simple.cok N (the number of trains)
Fischer Open-Kronos/Fischer/fischer.cok if Delta < Gamma Delta, Gamma
Stari Open-Kronos/Stari/stari.cok K
Producer-consumerprotocols/example-producer-consumer-v2.cok BufSize (the size of buffer)
Array Init arrays/param-array-init.cok N (number of processes), D (size of array asociated with a single process)
Array Copy arrays/param-array-copy.cok N (number of processes), D (size of array asociated with a single process)
Array Join arrays/param-array-join.cok N (number of processes), D (size of array asociated with a single process)


Adam Rogalewicz, rogalew@fit.vutbr.cz
Tomas Vojnar
Radu Iosif
Last changes: Jan. 2016