search

osate / ErrorModelV2

Old AADL EMV2 annex repository, kept for reference
3 stars 10 forks source link

PRISM bug for OSATE plugin #40

Closed sma350 closed 6 years ago

sma350 commented 10 years ago

Hi,

below I defined the correct form of the PRISM model defined in the previous issue named "syntaxical errors in the PRISM models generated":

dtmc

global bus_subsystem_i_instance_incoming_propagation_bpm: [ 0 .. 1] init 0; global bus_subsystem_i_instance_incoming_propagation_bpout: [ 0 .. 1] init 0; global bus_subsystem_i_instance_incoming_propagation_bpin: [ 0 .. 1] init 0;

module bus_subsystem_i_instance bus_subsystem_i_instance_state: [ 0 .. 1] init 0; [] bus_subsystem_i_instance_state=0 -> 1.0 : (bus_subsystem_i_instance_state'=1); [] bus_subsystem_i_instance_state=0 -> 1.0 : (bus_subsystem_i_instance_state'=1); [] bus_subsystem_i_instance_state=0 -> 1.0 : (bus_subsystem_i_instance_state'=1);

[] bus_subsystem_i_instance_state=1 & bus_subsystem_i_instance_incoming_propagation_bpm=0 & bus_subsystem_i_instance_incoming_propagation_bpout=0 & bus_subsystem_i_instance_incoming_propagation_bpin=0 -> (bus_subsystem_i_instance_state) + 1.0 : (bus_subsystem_i_instance_state'=1) & (bus_subsystem_i_instance_incoming_propagation_bpm'=0) & (bus_subsystem_i_instance_incoming_propagation_bpout'=0) & (bus_subsystem_i_instance_incoming_propagation_bpin'=0); endmodule

formula bus_subsystem_i_instance_is_operational = bus_subsystem_i_instance_state=0;

formula bus_subsystem_i_instance_is_failed = bus_subsystem_i_instance_state=1;

formula bus_subsystem_i_instance_incoming_propagation_bpout_get_noservice = bus_subsystem_i_instance_incoming_propagation_bpout=1;

formula bus_subsystem_i_instance_incoming_propagation_bpin_get_noservice = bus_subsystem_i_instance_incoming_propagation_bpin=1;

formula bus_subsystem_i_instance_incoming_propagation_bpm_get_noservice = bus_subsystem_i_instance_incoming_propagation_bpm=1;

rewards "steps" true : 1; endrewards formula NoService = 0;

I'll will try to fix this error in the plugin.

Smail.

reteprelief commented 6 years ago

PRISM export was a quick prototype and has been removed from the OSATE installation.