Skip to content
No description, website, or topics provided.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.
src Correct JANI output, minor debugging output tweaks. Mar 21, 2019
Makefile Add JSON output for JANI conversion. Oct 23, 2018
README Add support for model parameters. Nov 19, 2018


Dynamic Fault Tree Rare Event Simulator

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


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


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 (the
'next' branch is required at the time this README is written).

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.
--zvav		Use the Path-ZVA importance sampling technique.
--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
--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.
You can’t perform that action at this time.