Logic error in embedded-control error model states #8
Description
According to documentation the systems needs at least two operational sensors and at least one operational actuator. The logic implemented says that at least one operational actuator makes the system operational, and at least one failed actuator makes the system failed, so a condition can exist that makes the system operational and failed at the same time. This error also exists in the wiki.sei.cmu.edu page referenced in the model.
[(at least two sensors operational) or (a1.Operational or a2.Operational)]-> Operational;
[a1.Failed or a2.Failed]-> Failed;
Should be:
[(at least two sensors operational) and (a1.Operational or a2.Operational)]-> Operational;
[a1.Failed and a2.Failed]-> Failed;
osate/examples/embedded-control/aadl-model/embedded-control-advanced.aadl lines 283-284
osate/examples/embedded-control/aadl-model/embedded-control.aadl lines 217-218