examples

[astefano]

Hi again,

Could we please have a running example? And how to run it, currently, i get:

lacra@lacra-VirtualBox:~/tools/mlsolver/bin$ ./mlsolver --help PGSolver Collection Ver. 4.0: Parity Game Solver Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2016 http://tcsprojects.org Usage: pgsolver [options] [infile] Solves the parity game given in <infile>. If this argument is omitted it reads a game from STDIN. Options are -v <level> sets the verbosity level, valid arguments are 0 (quiet), 1 (default), 2 (verbose) and 3 (very verbose) --printsolonly causes the program to simply output a parsable solution -d <filename> output the solution as a coloured graph in dotty format into <filename> --printsolvedgame, -pg outputs the solved (!) game on STDOUT --parsesolution, -ps <filename> parses the solution to the game from FILE --justheatCPU, -jh suppress the printing of the strategies and the winning regions --verify, -ve verify solution using the universal solver (fast) --disableglobalopt, -dgo disable global optimization --disablesccdecomposition, -dsd disable scc decomposition --disablelocalopt, -dlo disable local optimization --disablespecialgames, -dsg disable optimized solving of special games --solverinfo output information about all available solvers --globallysolve, -global <solver> solves globally, valid solvers are bigstep dominiondec fpiter genetic guessstrategy modelchecker optstratimprov policyiter recursive smallprog stratimprdisc stratimprloc2 stratimprlocal stratimprove --locallysolve, -local <solver> <node> solves locally, valid solvers are modelchecker stratimprloc2 stratimprlocal --args, -x pass args to the solver (write '-x "--help"' to learn about available args (if there are any)) --generator, -gen <generator> "<args>" use generator, valid ones are cliquegame clusteredrg elevatorvergm jurdzinskigame laddergame langincl modelcheckerladder randomgame recursiveladder steadygame towersofhanoi

I tried to see if maybe the generators can be seen as examples, but not sure how to run correctly: lacra@lacra-VirtualBox:~/tools/mlsolver/bin$ ./mlsolver -gen modelcheckerladder ./mlsolver: option '-gen' needs an argument.

Cheers, lacramioara

[oliverfriedmann]

I've added an example to the README file.

[astefano]

i get bin/mlsolver: unknown option '-stenv'. what are, in fact, the arguments to mlsolver? (-h gives the ones for pgsolver, i assume).

[oliverfriedmann]

bin/mlsolver --help Modal Logic Solver 1.3 Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2017

Usage: mlsolver [options] [formula]

Options are --validity, -val Decides validity, valid arguments are pdl, mmc, ltmc, lmmc, ctlstar, ctl --satisfiability, -sat Decides satisfiability, valid arguments are pdl, mmc, ltmc, lmmc, ctlstar, ctl --modelchecking, -mc Decides modelchecking, valid arguments are pdl, mmc, ltmc, lmmc, ctlstar, ctl --transitionsystem, -ts Parses transition system --stdints, -stts Parses transition system from stdin --environment, -env Parses formula environment --stdinenv, -stenv Parses formula environment from stdin --option, -opt Adds options to decision procedure; available: ann : add decision game annotations comp : compact games ctlplus : use ctl plus optimization (experimental) prefersmall : prefer small subformulas preferlarge : prefer large subformulas woguarded : without guarded transformation --printgame, -pg Generates and prints the decision game --generatemodel, -gm Generates a (counter)model if applicable --verbose, -ve causes the program to be verbose --quiet, -qu causes the program to be quiet --pgsolver, -pgs use pgsolver with bigstep dominiondec fpiter genetic guessstrategy modelchecker optstratimprov policyiter recursive smallprog stratimprdisc stratimprloc2 stratimprlocal stratimprove --partialpgsolver, -ppgs use partial pgsolver with modelchecker stratimprloc2 stratimprlocal

[astefano]

strange, as i initially wrote, i get:

lacra@lacra-VirtualBox:~/tools/mlsolver$ bin/mlsolver -help PGSolver Collection Ver. 4.0: Parity Game Solver Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2016 http://tcsprojects.org Usage: pgsolver [options] [infile] Solves the parity game given in <infile>. If this argument is omitted it reads a game from STDIN. Options are -v <level> sets the verbosity level, valid arguments are 0 (quiet), 1 (default), 2 (verbose) and 3 (very verbose) --printsolonly causes the program to simply output a parsable solution -d <filename> output the solution as a coloured graph in dotty format into <filename> --printsolvedgame, -pg outputs the solved (!) game on STDOUT ...

[oliverfriedmann]

That is definitely PGSolver. Did you run make in the pgsolver subdirectory instead of the mlsolver directory?

[astefano]

no, no, i followed your instructions precisely (make from mlsolver). so i get in bin:

lacra@lacra-VirtualBox:~/tools/mlsolver$ ls bin ctlstarsudokugenerator elevatortsgenerator guarded_trafo_worst_case ltmcparitybuechigenerator mlsolver mucalcsudokugenerator pdlsudokugenerator philosopherstsgenerator

[oliverfriedmann]

I've adjusted some ambiguously named files - please try one more time. Not sure why we get different results, but it might be related to the order in which our system are enumerating files.

[astefano]

thanks a lot, now it works! one last question: what's the grammar for transition systems? (can't find where Tcstransitionparser.parse... is implemented...)

[oliverfriedmann]

Apologies for the lack of documentation, this is definitely something we need to work on.

In the meantime, formula parsing is in TCSLib: https://github.com/tcsprojects/tcslib/tree/master/src/formula/parser

[astefano]

ok, thanks! yep, some documentation would be great :) Please bear with me a little bit more... How should one interpret the output? For instance, there is no difference between checking true or [a]true.

lacra@lacra-VirtualBox:~/tools/mlsolver$ bin/mlsolver -mc pdl -ts ex.ts "<a>true" Modal Logic Solver 1.3 Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2017 Evaluating formula... 0.00 sec Using Modelchecking Procedure For PDL Starting procedure... Modelchecking Procedure For PDL

lacra@lacra-VirtualBox:~/tools/mlsolver$ bin/mlsolver -mc pdl -ts ex.ts "[a]true" Modal Logic Solver 1.3 Authors: Oliver Friedmann (University of Munich) and Martin Lange (University of Kassel), 2008-2017 Evaluating formula... 0.00 sec Using Modelchecking Procedure For PDL Starting procedure... Modelchecking Procedure For PDL

Shouldn't it output (un)sat?

Just for the reference, i just took a simple TS: lts 2; start 0; 0 a : 1; 1 b : 0;

True is "tt" (see parser). And you always have to specify a solver, e.g. -pgs recursive

[astefano]

ok, thanks a lot for all your help!