syntaxical errors in the PRISM generated models

Question

syntaxical errors in the PRISM generated models

Closed this issue 11 years ago · 5 comments

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.

Answer 1 · 2014-02-01T06:53:00.000Z

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

Answer 2 · 2014-02-03T12:58:59.000Z

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;

Answer 3 · 2014-02-03T13:27:21.000Z

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.

Answer 4 · 2014-02-03T16:09:50.000Z

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;

Answer 5 · 2019-03-15T03:31:48.000Z

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