PAMCSolver: A Satisfiability Solver for Probabilistic Alternating-Time Mu-Calculus

This README would normally document whatever steps are necessary to get your application up and running.

What is this repository for?

This project focuses on the satisfiability problem of PAMC. [Slides] [Paper] [Full version]

How to set up?

Jar packages you need to have in your own project:

antlr-4.4-complete.jar
dom4j-1.6.1.jar
com.microsoft.z3.jar
jgrapht-core-0.9.0.jar
and other basic jar packages.

Other tools you need to have in your project:

GOAL, our source code contains a version of GOAL;

Get source code of PAMCSolver

Download  

Running tests:

Any PAMC/AMC/PμTL expression is ok(detailed requirements you need to view the source code in Pamc.g4)
For example:
    PAMC:
    <1,2> >1/2 p & <3> >1/2 (~p | q) & [1,3] >2/5 (~p & ~q)
    AMC:
    <1,2> >=1/1 p & <3> >=1/1 (~p | q) & [1,3] >=1/1 (~p & ~q)
    PμTL:
    <> >1/2 p & <> >1/2 (~p | q) & <> >2/5 (~p & ~q)
Attention:
For my grammar file defining the Diamond(Box) expression in the form of '<' (INT (',' INT)*)* '>' op = ('>' | '>=' | '<' | '<=') FLOAT expr('[' (INT (',' INT)*)* ']' op = ('>' | '>=' | '<' | '<=') FLOAT expr) 
where FLOAT: INT '/' INT, so if you test on AMC sentences, you should write like this:<1,2> >=1/1 p & <3> >=1/1 (~p | q) & [1,3] >=1/1 (~p & ~q).
And the Mu(Nu) expressions are defined in the form of 'mu' ID '.' expr('nu' ID '.' expr), where ID : [a-zA-Z]+, so we advise you input test cases like Mu X.(expr1), Mu Y.(expr2) not Mu X1.(expr1), Mu X2.(expr2).
Sorry for this inconvenience, we will improve it instantly.
Also if you test on PμTL sentences the <A> op float Expr [B] op float Expr should all be replaced by [X Expr] op float, that are all the form of <> op float Expr.

 The Mu(Nu) expressions are defined in the form of 'mu' ID '.' expr('nu' ID '.' expr), where ID : [a-zA-Z]+, so we advise you input test cases like Mu X.(expr1), Mu Y.(expr2) not Mu X1.(expr1), Mu X2.(expr2).
Sorry for this inconvenience, we will improve it instantly.
Also if you test on PμTL sentences the <A> op float Expr [B] op float Expr should all be replaced by [X Expr] op float, that are all the form of <> op float Expr.

How to run?

This tool can be run either Unix or Linux.
The easiest way is that you just download the source code in your own workspace, and import it in the IDE you use usually, like Eclipse, or IDEA. However, 
some points you should take care:

1.Antlr4:
If you want to check the correctness of your own grammar g4 file, we advise you integrate the Antlr4 in your IDE, it not only helps you check the 
correctness of your grammar file, it also can build a AST tree when you input a sentence, which is vivid to observe the whole structure of the sentence 
and helpful to correct the g4 file if you have a wrong one.

2.Z3:
Z3, a theorem prover, that we advise you install it via compiling source code to obtain the jar package. You can validate whether Z3 installed succsessfully by 
tesing the examples in the Z3 source code. We give you some useful link below:
https://github.com/Z3Prover/z3
http://leodemoura.github.io/blog/2012/12/10/z3-for-java.html
If you report errors that "java.lang.UnsatisfiedLinkError: no z3java in java.library.path", you should make the LD_LIBRARY_PATH point to the directory 
where libz3java.so is located.