Error in the prism model generated when runtime N1|N2 is used for tasks

lesunb / CRGMToPRISM

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 generated when runtime N1|N2 is used for tasks #22

Closed gabrielasolano closed 6 years ago

gabrielasolano commented 6 years ago

The runtime N1|N2 represents the XOR decomposition.

When used with tasks, the prism model generated by GODA has only one module and doesn't represent the DTMC template stated by the article.

Check "Listing. 6" of GODA's article to understand more how the model should be.

gabrielasolano commented 6 years ago

Same error of issue https://github.com/lesunb/CRGMToPRISM/issues/19

Corrected by commit https://github.com/lesunb/CRGMToPRISM/commit/7c86ba75a75a1a602fb62d03085aeb3b8e26607c