syntaxical errors in the PRISM generated models

[sma350]

Hi,

first of all thank you for your help in my previous issue. I have a new problem with the PRISM models generated in OSATE.

When I used the model checker PRISM (version 4.1.beta 2-linux 64) to analyze the models generated in OSATE I found syntactic errors in the generated model ".pm" in some examples. I want to know what version of PRISM I have to use to analyze these PRISM models.

For information, I asked for help in the PRISM forum about the errors in the model example "embedded-control," here is the link of the problem and the solution that was given to me:

https://groups.google.com/forum/?fromgroups #! topic/prismmodelchecker/UmBLG9ur1n0

Best regards,

Smail.

[juli1]

Please explain which models you are using. Also, this might be a bug for OSATE plugins and not the examples repository.

[sma350]

hi, I have an error in the generated PRISM model of the embedded-control-advanced.aadl model (embedded-control folder):

######### PRISM Model

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'=0) + 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); -----> ERROR : Syntax error ("+", line 12, column 249)

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;

[juli1]

This is not an issue related to the example but rather to the plugin. Please provide the output model and/or fix to the plugin.

Thanks.

[sma350]

Above the correct form of the PRISM model :

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;

[geniusqu]

Hi,

first of all thank you for your help in my previous issue. I have a new problem with the PRISM models generated in OSATE.

When I used the model checker PRISM (version 4.1.beta 2-linux 64) to analyze the models generated in OSATE I found syntactic errors in the generated model ".pm" in some examples. I want to know what version of PRISM I have to use to analyze these PRISM models.

For information, I asked for help in the PRISM forum about the errors in the model example "embedded-control," here is the link of the problem and the solution that was given to me:

https://groups.google.com/forum/?fromgroups #! topic/prismmodelchecker/UmBLG9ur1n0

Best regards,

Smail. Can you tell me how to generate PRISM models using osate