In a nutshell, GODA (Goal-Oriented Dependability Analysis) is a framework for verification of goal models through probabilistic model checking, where contextual goal models are translated into PRISM and PARAM languages.
2
stars
6
forks
source link
Error in the prism model when runtime N1|N2 is used for goals #23
The runtime N1|N2 represents the XOR decomposition.
Although the DTMC model's template is correct, not every goal has its formula generated correctly.
For example, using the runtime [G2|G3|G4], the formulas are (now) printed as:
formula G2 = (sG2_T1=2 | sG3_T1=2 | sG4_T1=2);
formula G3 = ;
formula G4 = ;
The runtime N1|N2 represents the XOR decomposition.
Although the DTMC model's template is correct, not every goal has its formula generated correctly.
For example, using the runtime [G2|G3|G4], the formulas are (now) printed as: formula G2 = (sG2_T1=2 | sG3_T1=2 | sG4_T1=2); formula G3 = ; formula G4 = ;