I cannot run analyses for DFTs with PAND gates with any backend. The issue seems to be in the translation done by dft2lntc.

To reproduce, call with options -t 10 -p on the following DFT:

toplevel "TLE";
"TLE" pand "B1" "B2";
"B1" lambda=5.11e-5;
"B2" lambda=1.11e-4;

I get the following warnings and errors:

~$ dftcalc -t 10 foo.dft -p
:: ** OUTPUT of foo.0.dft2lntc.out **
:error:
:: ** END output of foo.0.dft2lntc.out **
:: ** OUTPUT of foo.0.dft2lntc.err **
:error::: Running dft2lntc...
/home/hobborg/UT/repos/DFT_benchmarks/other/fault_trees/foo.dft:2.1-21:warning:Unable to create AUT file for this node: `TLE'
/home/hobborg/UT/repos/DFT_benchmarks/other/fault_trees/foo.dft:3.1-20:error:Could not generate BCG file `be_cold_aa.bcg' for node type `be'
:: Finished. 1 errors and 1 warnings.

In the master branch, there is a missing "end:" tag in the following files when compiling in the CADP library:

dftcalc.cpp (between lines 268 and 269)
dfttest.cpp (between lines 250 and 251)

Simple example (with --imrmc)
toplevel "A"; "A" lambda=1 res=1;

This translates to an empty automaton, which IMRMC does not know how to handle.

When calling with "-m" option, the output print shows MTTF(...) = <val> for all analysis options passed. The output values <val> are not overriden, only the output header is.

To reproduce run with options -p -s -m and -p -m -t 10 on the following FT:

toplevel "TLE";
"TLE" and "B1" "B2";
"B1" lambda=0.09 repair=333.33;
"B2" lambda=0.12 repair=333.33;

When a SPARE gate has cold Spares that are shared or consist out of subtrees, the smart Semantics will erroneously mark them as active, and thus activate the cold spares from the beginning.

Temporary solution:
uncomment line 578 (dft->applySmartSemantics();) in dft2lntc.cpp

This will deactivate the smart semantics.

The description of the res attribute for BEs as found in this page doesn't seem to be implemented.

To see that, run the tool with options -p -s -m on the following FT, and then again on that FT but replacing res=1.0 by res=0.0. The expected behaviour is that for run with res=0.0 the MTTF remains the same but the unavailability increases: that is not happening and for both cases the exact same results are given.

toplevel "TLE";
"TLE" and "B1" "B2";
"B1" lambda=0.09 res=1.0 repair=1.3;
"B2" lambda=0.12 res=1.0 repair=1.3;

Furthermore, res should be a probability value in the closed interval [0.0,1.0]. However any value is currently accepted (and seemingly ignored) by the tool. To reproduce run with the options as above on the same FT with res=80085.

When running analyses with Storm as backend (default), if the result uses scientific notation then the numbers before the "e" seem to be truncated from standard output.

To reproduce, call with options -t 10 -p and -t 10 -p --imrmc on the following FT:

toplevel "TLE";
"TLE" and "B1" "B2";
"B1" lambda=5.11e-5;
"B2" lambda=1.11e-4;

With Storm I get the output P(..., P(F[<=10] FAIL), 10, fails)=e-7 whereas with IMRMC I get instead P(..., P(F[<=10] FAIL), 10, fails)=5.667504978095[299; 302]e-7

BEs with an attached inspection module but no interval=N attribute cause IMPOSSIBLE labels to survive composition and hiding, resulting in a fatal error.

Proposed solution: Treat such BEs as having an interval above the number of phases, thereby omitting the actual inspection but allowing the BE to be repaired if something else causes the inspection to act.

Transient states with meaningful properties (e.g., a state reachable by a FAIL transition from which an ONLINE transition can immediately be taken) currently cause either an error or are ignored when translating to a CTMC. The translators need to correctly mark the state following the ONLINE transition as having experience a transient failure. The model-checker queries should take this new marking into account.

Add an attribute transient=P to BEs. When the BE fails, with probability P, it should emit a failure signal immediately followed (i.e., with no intervening Markovian or timed transitions), but a repaired signal.

I'm trying to run the latest DFTCalc (529c7fb) with the latest DFTRES (utwente-fmt/DFTRES@bc69223) and Storm 1.6.4 (moves-rwth/storm@6f39d43).

When I run dftcald without the --exact flag, I get

commandline:warning:CADP mode not compiled in, enabling --exact

and Storm returns and exact solution. Thus, I can't get a floating-point result, even if I specify an error bound with -E.

Due to the large size of the models I want to analyse, I'd like run Storm with floating-point arithmetic.

It seems the warning is emitted in

and runExact is forced in

which subsequently passes --exact to Storm.

I removed latter lines above, and DFTCalc with Storm seems to produce correct floating-point solutions. Are there any pitfalls with this calculation approach? It would be nice if DFTCalc supported non-exact calculation without CADP out of the box.

Automata for gates currently behave nondeterministically when a FAIL signal of a child is immediately followed by an ONLINE signal. The gate should always emit its own FAIL signal if the child failure should cause a failure, possibly followed as well by its own ONLINE.