Accessing transition matrix by action
35 views
Skip to first unread message
Calvin Chau
Apr 7, 2019, 3:05:09 PM4/7/19
to PRISM model checker developers
Hello everyone!
I am new to prism and for my thesis I am supposed to extend prism by the ability to compute a bisimulation matrix. I am considering an action deterministic MDP and need to access the transition matrix of every action.
Currently I am considering this model:
mdp
module M1
x:[0..6];
[a] x=0 -> 1.0:(x'=1);
[a] x=1 -> 0.5:(x'=2) + 0.5:(x'=3);
[b] x=2 -> 1.0:(x'=2);
[c] x=3 -> 1.0:(x'=3);
[a] x=4 -> 1.0:(x'=2);
[a] x=5 -> 1.0:(x'=3);
[a] x=6 -> 0.5:(x'=4) + 0.5:(x'=5);
endmodule
init x=0 | x=6 endinit
module M1
x:[0..6];
[a] x=0 -> 1.0:(x'=1);
[a] x=1 -> 0.5:(x'=2) + 0.5:(x'=3);
[b] x=2 -> 1.0:(x'=2);
[c] x=3 -> 1.0:(x'=3);
[a] x=4 -> 1.0:(x'=2);
[a] x=5 -> 1.0:(x'=3);
[a] x=6 -> 0.5:(x'=4) + 0.5:(x'=5);
endmodule
init x=0 | x=6 endinit
and for action c for example I would like to get the following matrix:
0 0 0 0 0 0 0
0 0 0 0 0 0 0
0 0 0 0 0 0 0
0 0 0 1 0 0 0
0 0 0 0 0 0 0
0 0 0 0 0 0 0
0 0 0 0 0 0 0
Is there any simple way of doing this? I am sorry if I am missing something obvious.
Thank you very much in advance!
Dave Parker
Apr 9, 2019, 5:35:43 AM4/9/19
to calvinc...@gmail.com, PRISM model checker developers
Hi,
Welcome! PRISM has several distinct model checking engines which are
rather different in nature. For prototypes, people often build on the
"explicit" engine, which is pure Java and mainly based on sparse matrix
data structures for porobabilistic models. There are also "symbolic"
engines. These can be more efficient for large models, but there is a
much steeper learning curve for development. Let us know which you plan
to use (my suggestion would be "explicit") and then I can send some
pointers.
Best wishes,
Dave
On 07/04/2019 21:05, calvinc...@gmail.com wrote:
> Hello everyone!
>
> I am new to prism and for my thesis I am supposed to extend prism by the
> ability to compute a bisimulation matrix. I am considering an action
> deterministic MDP and need to access the transition matrix of every action.
>
> Currently I am considering this model:
>
> *mdp
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
> prismmodel...@googlegroups.com
> <mailto:prismmodel...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker-dev.
Welcome! PRISM has several distinct model checking engines which are
rather different in nature. For prototypes, people often build on the
"explicit" engine, which is pure Java and mainly based on sparse matrix
data structures for porobabilistic models. There are also "symbolic"
engines. These can be more efficient for large models, but there is a
much steeper learning curve for development. Let us know which you plan
to use (my suggestion would be "explicit") and then I can send some
pointers.
Best wishes,
Dave
On 07/04/2019 21:05, calvinc...@gmail.com wrote:
> Hello everyone!
>
> I am new to prism and for my thesis I am supposed to extend prism by the
> ability to compute a bisimulation matrix. I am considering an action
> deterministic MDP and need to access the transition matrix of every action.
>
> Currently I am considering this model:
>
>
> module M1
>
> x:[0..6];
>
> [a] x=0 -> 1.0:(x'=1);
> [a] x=1 -> 0.5:(x'=2) + 0.5:(x'=3);
> [b] x=2 -> 1.0:(x'=2);
> [c] x=3 -> 1.0:(x'=3);
> [a] x=4 -> 1.0:(x'=2);
> [a] x=5 -> 1.0:(x'=3);
> [a] x=6 -> 0.5:(x'=4) + 0.5:(x'=5);
>
> endmodule
>
> init x=0 | x=6 endinit*
> module M1
>
> x:[0..6];
>
> [a] x=0 -> 1.0:(x'=1);
> [a] x=1 -> 0.5:(x'=2) + 0.5:(x'=3);
> [b] x=2 -> 1.0:(x'=2);
> [c] x=3 -> 1.0:(x'=3);
> [a] x=4 -> 1.0:(x'=2);
> [a] x=5 -> 1.0:(x'=3);
> [a] x=6 -> 0.5:(x'=4) + 0.5:(x'=5);
>
> endmodule
>
>
> and for action c for example I would like to get the following matrix:
>
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 1 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
>
> Is there any simple way of doing this? I am sorry if I am missing
> something obvious.
>
> Thank you very much in advance!
>
> --
> and for action c for example I would like to get the following matrix:
>
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 1 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
> 0 0 0 0 0 0 0
>
> Is there any simple way of doing this? I am sorry if I am missing
> something obvious.
>
> Thank you very much in advance!
>
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To post to this group, send email to
> prismmodel...@googlegroups.com
> <mailto:prismmodel...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/prismmodelchecker-dev.
Calvin Chau
Apr 9, 2019, 4:12:13 PM4/9/19
to PRISM model checker developers
Hello Dave,
thanks for you response. Yes, I already tried to build the explicit model, but somehow I am getting a ClassCastException, namely:
"class explicit.MDPSparse cannot be cast to class explicit.MDPSimple".
Best Regards
Calvin
Am Dienstag, 9. April 2019 11:35:43 UTC+2 schrieb Dave Parker:
Hi,
Welcome! PRISM has several distinct model checking engines which are
rather different in nature. For prototypes, people often build on the
"explicit" engine, which is pure Java and mainly based on sparse matrix
data structures for porobabilistic models. There are also "symbolic"
engines. These can be more efficient for large models, but there is a
much steeper learning curve for development. Let us know which you plan
to use (my suggestion would be "explicit") and then I can send some
pointers.
Best wishes,
Dave
> an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <mailto:prismmodelchecker-dev+unsub...@googlegroups.com>.
Dave Parker
Apr 11, 2019, 8:21:19 AM4/11/19
to calvinc...@gmail.com, PRISM model checker developers
Hi Calvin,
The explicit engine can build and solve the MDP using either MDPSparse
or MDPSimple. The former is mutable and slightly less efficient, so the
former should be the default. How did you trigger this exception?
Dave
On 09/04/2019 22:12, calvinc...@gmail.com wrote:
> Hello Dave,
>
> thanks for you response. Yes, I already tried to build the explicit
> model, but somehow I am getting a ClassCastException, namely:
> "class explicit.MDPSparse cannot be cast to class explicit.MDPSimple".
>
> Best Regards
> Calvin
>
> Am Dienstag, 9. April 2019 11:35:43 UTC+2 schrieb Dave Parker:
>
> Hi,
>
> Welcome! PRISM has several distinct model checking engines which are
> rather different in nature. For prototypes, people often build on the
> "explicit" engine, which is pure Java and mainly based on sparse matrix
> data structures for porobabilistic models. There are also "symbolic"
> engines. These can be more efficient for large models, but there is a
> much steeper learning curve for development. Let us know which you plan
> to use (my suggestion would be "explicit") and then I can send some
> pointers.
>
> Best wishes,
>
> Dave
>
> > an email to prismmodelchecke...@googlegroups.com
> <javascript:>
> > <mailto:prismmodelchecke...@googlegroups.com
> <javascript:>>.
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> <https://groups.google.com/group/prismmodelchecker-dev>.
> <mailto:prismmodelchecke...@googlegroups.com>.
The explicit engine can build and solve the MDP using either MDPSparse
or MDPSimple. The former is mutable and slightly less efficient, so the
former should be the default. How did you trigger this exception?
Dave
On 09/04/2019 22:12, calvinc...@gmail.com wrote:
> Hello Dave,
>
> thanks for you response. Yes, I already tried to build the explicit
> model, but somehow I am getting a ClassCastException, namely:
> "class explicit.MDPSparse cannot be cast to class explicit.MDPSimple".
>
> Best Regards
> Calvin
>
> Am Dienstag, 9. April 2019 11:35:43 UTC+2 schrieb Dave Parker:
>
> Hi,
>
> Welcome! PRISM has several distinct model checking engines which are
> rather different in nature. For prototypes, people often build on the
> "explicit" engine, which is pure Java and mainly based on sparse matrix
> data structures for porobabilistic models. There are also "symbolic"
> engines. These can be more efficient for large models, but there is a
> much steeper learning curve for development. Let us know which you plan
> to use (my suggestion would be "explicit") and then I can send some
> pointers.
>
> Best wishes,
>
> Dave
>
> <javascript:>
> > <mailto:prismmodelchecke...@googlegroups.com
> <javascript:>>.
> > To post to this group, send email to
> > prismmodel...@googlegroups.com <javascript:>
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> <https://groups.google.com/group/prismmodelchecker-dev>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> <mailto:prismmodelchecke...@googlegroups.com>.
Calvin Chau
Apr 14, 2019, 1:00:50 PM4/14/19
to PRISM model checker developers
Hello Dave,
I am accessing the prism api programmatically. First I initialize and parse the model as shown in PrismTest.java. Then I call prism.buildModelExplicit(modulesFiles) and that is where the exception is thrown.
Best regards
Calvin
Am Donnerstag, 11. April 2019 14:21:19 UTC+2 schrieb Dave Parker:
Hi Calvin,
The explicit engine can build and solve the MDP using either MDPSparse
or MDPSimple. The former is mutable and slightly less efficient, so the
former should be the default. How did you trigger this exception?
Dave
> > an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <javascript:>
> > <mailto:prismmodelchecker-dev+unsub...@googlegroups.com
> <javascript:>>.
> > To post to this group, send email to
> > prismmodel...@googlegroups.com <javascript:>
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > Visit this group at
> https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <mailto:prismmodelchecker-dev+unsub...@googlegroups.com>.
Dave Parker
Apr 15, 2019, 6:58:28 PM4/15/19
to calvinc...@gmail.com, PRISM model checker developers
Not sure why that would be. The most up-to-date examples of accessing
PRISM programmatically are here, in case that helps:
https://github.com/prismmodelchecker/prism-api
If you can post/send the code that is failing, I can look.
Best wishes,
Dave
On 14/04/2019 19:00, calvinc...@gmail.com wrote:
> Hello Dave,
>
> I am accessing the prism api programmatically. First I initialize and
> parse the model as shown in PrismTest.java. Then I call
> prism.buildModelExplicit(modulesFiles) and that is where the exception
> is thrown.
>
> Best regards
> Calvin
>
> Am Donnerstag, 11. April 2019 14:21:19 UTC+2 schrieb Dave Parker:
>
> Hi Calvin,
>
> The explicit engine can build and solve the MDP using either MDPSparse
> or MDPSimple. The former is mutable and slightly less efficient, so the
> former should be the default. How did you trigger this exception?
>
> Dave
>
> prismmodelchecke...@googlegroups.com <javascript:>
> > <javascript:>
> > > <mailto:prismmodelchecke...@googlegroups.com
> <javascript:>
> <javascript:>
> > <mailto:prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
PRISM programmatically are here, in case that helps:
https://github.com/prismmodelchecker/prism-api
If you can post/send the code that is failing, I can look.
Best wishes,
Dave
On 14/04/2019 19:00, calvinc...@gmail.com wrote:
> Hello Dave,
>
> I am accessing the prism api programmatically. First I initialize and
> parse the model as shown in PrismTest.java. Then I call
> prism.buildModelExplicit(modulesFiles) and that is where the exception
> is thrown.
>
> Best regards
> Calvin
>
> Am Donnerstag, 11. April 2019 14:21:19 UTC+2 schrieb Dave Parker:
>
> Hi Calvin,
>
> The explicit engine can build and solve the MDP using either MDPSparse
> or MDPSimple. The former is mutable and slightly less efficient, so the
> former should be the default. How did you trigger this exception?
>
> Dave
>
> > <javascript:>
> > > <mailto:prismmodelchecke...@googlegroups.com
> <javascript:>
> > <javascript:>>.
> > > To post to this group, send email to
> > > prismmodel...@googlegroups.com <javascript:>
> > > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > > Visit this group at
> > https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>
> > <https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>>.
> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "PRISM model checker developers" group.
> > To unsubscribe from this group and stop receiving emails from it,
> send
> > an email to prismmodelchecke...@googlegroups.com
> > > To post to this group, send email to
> > > prismmodel...@googlegroups.com <javascript:>
> > > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > > Visit this group at
> > https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>
> > <https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>>.
> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "PRISM model checker developers" group.
> > To unsubscribe from this group and stop receiving emails from it,
> send
> <javascript:>
> > <mailto:prismmodelchecke...@googlegroups.com
> <javascript:>>.
> > To post to this group, send email to
> > prismmodel...@googlegroups.com <javascript:>
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > Visit this group at
> https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> > To post to this group, send email to
> > prismmodel...@googlegroups.com <javascript:>
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > Visit this group at
> https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> <mailto:prismmodelchecke...@googlegroups.com>.
Calvin Chau
Apr 16, 2019, 5:51:29 AM4/16/19
to PRISM model checker developers
Hey Dave,
this is my code:
public class Bisimulation {
public static void main(String[] args) {
new Bisimulation().go(args);
}
public void go(String args[]) {
try {
//Initialize
PrismLog mainLog = new PrismFileLog("stdout");
Prism prism = new Prism(mainLog);
prism.initialise();
//Parse model
ModulesFile modulesFile = prism.parseModelFile(new File(args[0]));
prism.loadPRISMModel(modulesFile);
//Get model
prism.buildModelExplicit(modulesFile);
Model model = prism.getBuiltModel();
}
catch(FileNotFoundException e) {
System.out.println("Error: " + e);
System.exit(1);
}
catch(PrismException e) {
System.out.println("Error: " + e);
System.exit(1);
}
}
}
public static void main(String[] args) {
new Bisimulation().go(args);
}
public void go(String args[]) {
try {
//Initialize
PrismLog mainLog = new PrismFileLog("stdout");
Prism prism = new Prism(mainLog);
prism.initialise();
//Parse model
ModulesFile modulesFile = prism.parseModelFile(new File(args[0]));
prism.loadPRISMModel(modulesFile);
//Get model
prism.buildModelExplicit(modulesFile);
Model model = prism.getBuiltModel();
}
catch(FileNotFoundException e) {
System.out.println("Error: " + e);
System.exit(1);
}
catch(PrismException e) {
System.out.println("Error: " + e);
System.exit(1);
}
}
}
I hoping I am not missing something obvious.
Best regards
Calvin
Am Dienstag, 16. April 2019 00:58:28 UTC+2 schrieb Dave Parker:
Not sure why that would be. The most up-to-date examples of accessing
PRISM programmatically are here, in case that helps:
https://github.com/prismmodelchecker/prism-api
If you can post/send the code that is failing, I can look.
Best wishes,
Dave
> prismmodelchecker-dev+unsub...@googlegroups.com <javascript:>
> > <javascript:>
> > > <mailto:prismmodelchecker-dev+unsub...@googlegroups.com
> <javascript:>
> > <javascript:>>.
> > > To post to this group, send email to
> > > prismmodel...@googlegroups.com <javascript:>
> > > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > > Visit this group at
> > https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>
> > <https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>>.
> >
> > --
> > You received this message because you are subscribed to the Google
> > Groups "PRISM model checker developers" group.
> > To unsubscribe from this group and stop receiving emails from it,
> send
> > an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <javascript:>
> > <mailto:prismmodelchecker-dev+unsub...@googlegroups.com
> <javascript:>>.
> > To post to this group, send email to
> > prismmodel...@googlegroups.com <javascript:>
> > <mailto:prismmodel...@googlegroups.com <javascript:>>.
> > Visit this group at
> https://groups.google.com/group/prismmodelchecker-dev
> <https://groups.google.com/group/prismmodelchecker-dev>.
>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecker-dev+unsub...@googlegroups.com
> <mailto:prismmodelchecker-dev+unsub...@googlegroups.com>.
Dave Parker
Apr 16, 2019, 6:15:22 AM4/16/19
to calvinc...@gmail.com, PRISM model checker developers
Replace:
> prism.buildModelExplicit(modulesFile);
> Model model = prism.getBuiltModel();
with:
prism.setEngine(Prism.EXPLICIT);
prism.buildModel();
explicit.Model model = prism.getBuiltModelExplicit();
Hope that helps.
Dave
> prism.buildModelExplicit(modulesFile);
> Model model = prism.getBuiltModel();
prism.setEngine(Prism.EXPLICIT);
prism.buildModel();
explicit.Model model = prism.getBuiltModelExplicit();
Hope that helps.
Dave
Calvin Chau
Apr 16, 2019, 6:28:16 PM4/16/19
to PRISM model checker developers
Hello Dave,
it worked out, thanks a lot!
Best regards
Calvin
Reply all
Reply to author
Forward
0 new messages