There is a problem for getting properties on the EMV2 side. There is the issue:
If we instantiate the system complete.dual from test3_1_CTMC.aadl and generate the PRISM model, the probability assigned to the Failure event of the sensor (defined in the root instance) is processed correctly.
If we instantiate the complete.dual from test3_CTMC.aadl and generate the PRISM model, the probability is not shown in the generated PRISM model. The difference with the previous model is that the property is not defined in the root instance system but just in each subcomponent.
The following gist contains the model to reproduce the bug.
juli1
commented
11 years ago
There is a problem for getting properties on the EMV2 side. There is the issue: If we instantiate the system complete.dual from test3_1_CTMC.aadl and generate the PRISM model, the probability assigned to the Failure event of the sensor (defined in the root instance) is processed correctly.
If we instantiate the complete.dual from test3_CTMC.aadl and generate the PRISM model, the probability is not shown in the generated PRISM model. The difference with the previous model is that the property is not defined in the root instance system but just in each subcomponent.
The following gist contains the model to reproduce the bug.
https://gist.github.com/juli1/6176839