README

Dynamic Fault Tree Rare Event Simulator
=======================================

This program uses importance sampling to improve the estimations by
Monte Carlo simulations of (repairable) dynamic fault trees.


Compilation
-----------

Running 'make jar' should create the DFTRES.jar program.

Use
---

The standard syntax is:

java -jar DFTRES.jar [options] [<input>.exp | <input>.jani | <input.dft>]

NOTE: input from .dft files requires a working DFTCalc version.

Supported options are:
-s <N>		Seed for the random number generator.
-n <N>		Perform at most N simulations (exactly N unless a time
		bound is also provided).
-t <T>		Perform simulations for at most approximately T seconds.
--relErr <R>	Perform simulations to obtain a relative error of at
		most R.
-a		Analyze system availability (i.e., fraction of time the
		system is in unfailed states).
-r <B>		Perform reliability analysis with time bound B units
		(i.e., estimate the probability that no system failure
		occurs within B units time).
--mc		Use the standard Monte Carlo simulator without
		importance sampling.
--zvad		Use the Path-ZVA-d importance sampling technique.
--zvav		Use the Path-ZVA-v importance sampling technique.
--zvat		Use the Path-ZVA-t importance sampling technique
                (variation on ZVA-v, only potentially better for
                time-bounded reachability queries).
--def <C> <V>	Define the constant named C as the value V, overriding
		any definitions in the input file.
--export-jani <output.jani>	Export the model the specified jani
                           	file.
--export-tralab <output>	Export the model to <output>.tra and
                        	<output>.lab explicit-state files.
--prop		Analyze only the specified JANI property (can be used
		multiple times to analyze multiple properties.)
--json		Output data in JSON format.