This is the latest PDSolver webpage (29th October 2010). The original page and downloads submitted to Spin 2010 are available here.

PDSovler is a tool for evaluating both mu-calculus formulas over pushdown systems and pushdown parity games. It is an explicit state OCaml implementation of algorithms presented at Concur [Concur09] and appearing in Information and Computation [I&C10]. We also extend these algorithms to support backwards modalities [Backwards10] and allow the analysis to be restricted to reachable configurations.

An earlier version of this tool has been presented at SPIN 2010 [Spin10]. Below we provide examples of control flow graphs extracted, using the Soot Framework, from the DaCapo Benchmark Suite (Version 9.12). We distribute the tool with some Soot libraries. Up-to-date versions can be obtained from the Soot homepage. We do not distribute a copy of the DaCapo benchmarks.

This tool is maintained by Matthew Hague. Any queries/bugs/comments/&c. can be directed to Matthew Hague * comlab ox ac uk (with * = @ and spaces are .).

Download the latest versions. Previous versions are available from the Change Log.

- pdsolver-1.1.1.tgz
- The OCaml sources for PDSolver.
- pdsolver-examples-1.0.0.tgz
- An extended set of examples used as benchmarks in [Spin10].
- jimpletopdsolver-1.0.0.tgz
- A Java program for extracting pushdown control flow graphs with use/define information, used to create many of the examples above.
- jimpletopdsolver-examples-1.0.0.tgz
- An extended set of examples used as benchmarks in [Spin10]. See below for notes on usage.

PDSolver requires

- OCaml 3.10.1 [homepage], and
- OMake 0.9.8.5 (release 3) [homepage].

JimpleToPDSolver requires

- Java 1.6 [homepage], and
- Ant 1.7 [homepage].

We provide a short guide to getting started in Linux.

Download pdsolver.tgz and run the
following commands from the directory containing pdsolver.tgz.

```
tar xzf pdsolver.tgz
cd PDSolver
omake
```

If successful, we can evaluate an example.
./src/main/pdsolver.opt examples/journalInteresting.pdmu

To run the examples from the SPIN submission, first download pdsolver-examples.tgz to the
same directory as pdsolver.tgz. Then run the commands below (for
example).

```
tar xzf pdsolver-examples.tgz
cd PDSolver
./src/main/pdsolver.opt -o avroraReg.out -r csinit examples/avroraReg.pdmu
```

Here, `-o avroraReg.out`

specifies an output file, and
`-r csinit`

restricts the analysis to configurations
reachable from the initial configuration `<csinit, #>`

,
where the hash marks the bottom of the stack.
Download jimpletopdsolver.tgz and, from
the directory that contains it, run the following commands.

```
tar xzf jimpletopdsolver.tgz
cd JimpleToPDSolver
ant compile
```

If successful, you can then create an example pushdown system with
use/define information.
./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"

This generates a pushdown system with use/define information, but does
not add a mu-calculus formula. Open `dataflow.out`

and add
Mu Property:
!(
(nu X . (!csend &
[@def__examples_Dataflow__int_i_]ff
&
[\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_]X))
&
~[\def__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_](nu
Y.(mu Z. csend |
<@def__examples_Dataflow__int_i_>tt |
<\use__examples_Dataflow__int_i_ usedef__examples_Dataflow__int_i_>Z) &
~[\def__examples_Dataflow__int_i_ _usedef__examples_Dataflow__int_i_]Y)
)

to the end of the file, saving the file as `dataflow.pdmu`

. This is the dataflow example
from the Spin submission. We can generate the denotation of the
property by running the file through pdsolver, as in the extended
examples section above.
unzip dacapo-9.12-bach.jar 'jar/*' -d JimpleToPDSolver/lib/

Next download jimpletopdsolver-examples.tgz,
and save it in the same directory as jimpletopdsolver.tgz. Then extract
the examples.
tar xzf jimpletopdsolver-examples.tgz

Then recompile the sources and run an example.
cd JimpleToPDSolver
ant compile
./JimpleToPDSolver -f avroraReg.out "<examples.AvroraReg: void main(java.lang.String[])>"

Finally, add a mu property to `avroraReg.out`

as in the
previous example.
In the following, we assume familiarity with pushdown systems, parity games and mu-calculus.

To obtain usage information on PDSolver, run

```
./src/main/pdsolver.opt --help
```

There are a wealth of command line options, most of which we recommend
you ignore. The most important options are `--output-file`

,
`--output-format`

, `--check-type`

and
`--reachable`

.
The standard invocation command is

```
./src/main/pdsolver.opt -o <outfile> <infile>
```

where `outfile`

specifies where to write the output, and
`infile`

where to find the input problem. The type of
problem is determined by the file extension: `pdg`

for a
pushdown parity game, and `pdmu`

for a pushdown system and
mu-calculus problem. Common to both is a description of a pushdown
system. This takes the following form.
Rules:
p a -> q _;
p a -> q b;
p a -> q b c;
. . .

for pop, rewrite and push operations respectively, where `p`

and `q`

are control states, and `a`

,
`b`

and `c`

are stack characters. Note, a word of any
length may be specified. E.g. `p a -> q b c d e f;`

. The
stack character `#`

is a special character denoting the
bottom of the stack. This symbol cannot be added to, or removed from
the stack. Note that the alphabet of the system is inferred from the
pushdown rules and the `Interesting Configurations`

section
described below.
An example `pdg`

file (`examples/ArnaudInteresting.pdg`

) is shown below.

```
Rules:
p # -> f #;
p a -> p _;
f a -> p a;
f a -> f a a;
f # -> f #;
Control States:
p Abelard 1;
f Abelard 2;
Interesting Configurations:
p a a a #;
p #;
```

The pushdown system is described as above. The ```
Control
State
```

section specifies, for each control state, whether the
state is owned by `Eloise`

or `Abelard`

, and the
colour of the state. The `Interesting Configurations`

section identifies which configurations we are particularly interested
in. Note that each configuration ends with the `#`

symbol,
indicating the bottom of the stack. Additionally, this section may be
omitted, as in the example file `examples/Arnaud.pdg`

.
Running the command

```
./src/main/pdsolver.opt examples/Arnaud.pdg
```

yields the output below, which describes Eloise's winning region.
Done.
4 States: { q* qe (f,1) (p,1) }
Initial States: { (f,1) (p,1) }
Final States: { qe }
Transitions:
q* -#-> { { qe } }
q* -a-> { { q* } }
(f,1) -#-> { { qe } }
(f,1) -a-> { { q* (p,1) } }
(p,1) -#-> { { qe } }
(p,1) -a-> { { (p,1) } }
Interesting Configurations:
p a a a # : true
p # : true
Total time: 0.001999 Check time: 0.001999
Gather stats time: 0. Final opt time: 0.
Ma states: 4 Ma trans: 6
Max states: 0 Max trans: 0
Controls: 2 Characters: 2 Transitions: 5
Colours: 2

That is, an automaton with four states. The most important states are
`(f,1)`

and `(p,1)`

since these are initial
states and, for example, a
configuration `<p, w>`

is in Eloise's winning region if
`w`

is accepted from `(p,1)`

. In general, a
configuration `<p, w>`

is accepted if `w`

is
accepted from the initial state whose first component is
`p`

.
We describe the transitions. As an example, take a transition
`q -a-> { { q1 q2 } { q3 } }`

. This means the automaton has
two `a`

transitions from the state `q`

. The first
is an alternating transition to both `q1`

and
`q2`

. The second is a standard non-deterministic transition
to `q3`

.

The second section of output, titled ```
Interesting
Configurations
```

, tells us whether the configurations specified in
the input file are in the winning region described above. The remainder
of the output shows statistics on the input, runtime, and result. Note
that the zero entries are zero because we did not specify
`--gather-stats`

on the command line.

An example `pdmu`

input file
(`examples/journalInteresting.pdmu`

) follows.

```
Rules:
p a -> p _;
p # -> f #;
f # -> f #;
f a -> f a a;
f a -> p a;
Interesting Configurations:
p a a a #;
Mu Property:
(mu Z1 . (nu Z2 . ((p & []Z1) | (f & []Z2))))
Propositions:
p a p;
p # p;
f a f;
f # f;
```

The `Rules`

and `Interesting Configurations`

sections are as described above. Atomic propositions are specified in
the `Propositions`

section, taking the following form.
p a x y z . . .;

This line specifies that whenever the pushdown system has control state
`p`

and top of stack character `a`

, the atomic
propositions `x`

, `y`

and `z`

are true.
All other propositions are false.
The syntax of the mu-calculus is described below. Note that to ensure
the correct scoping of fixed points, we recommend putting all
expressions `mu Z . f`

and `nu Z . f`

in
parenthesis. That is `(mu Z . f)`

and ```
(nu Z .
f)
```

.

`x` |
Atomic propositions begin with a lowercase character. |

`Z` |
Variables begin with an uppercase character. |

`f1 & f2` |
The conjunction of formulas `f1` and `f2` . |

`f1 | f2` |
The disjunction of formulas `f1` and `f2` . |

`!f1` |
The negation of `f1` . |

`<>f1` |
The forward diamond modality for `f1` . |

`<@x1 x2 . . .>f1` |
The forward diamond modality for `f1` , parameterised
by the propositions `x1` , `x2` , &c.. |

`<\x1 x2 . . .>f1` |
The forward diamond modality for `f1` , parameterised
by all propositions other than `x1` , `x2` , &c.. |

`[]f1` |
The forward box modality for `f1` . |

`[@x1 x2 . . .]f1` |
The forward box modality for `f1` , parameterised
by the propositions `x1` , `x2` , &c.. |

`[\x1 x2 . . .]f1` |
The forward box modality for `f1` , parameterised
by all propositions other than `x1` , `x2` , &c.. |

`~<>f1` |
The backward diamond modality for `f1` . |

`~<@x1 x2 . . .>f1` |
The backward diamond modality for `f1` , parameterised
by the propositions `x1` , `x2` , &c.. |

`~<\x1 x2 . . .>f1` |
The backward diamond modality for `f1` , parameterised
by all propositions other than `x1` , `x2` , &c.. |

`~[]f1` |
The backward box modality for `f1` . |

`~[@x1 x2 . . .]f1` |
The backward box modality for `f1` , parameterised
by the propositions `x1` , `x2` , &c.. |

`~[\x1 x2 . . .]f1` |
The backward box modality for `f1` , parameterised
by all propositions other than `x1` , `x2` , &c.. |

`(mu Z . f1)` |
The least fixed point of `Z` in `f1` . |

`(nu Z . f1)` |
The greatest fixed point of `Z` in
`f1` . |

The JimpleToPDSolver tool provides very limited functionality. To
extract a pushdown system from a Java program, first make sure that the
program classes are available in the classpath.

```
export CLASSPATH="<path to program classes>:$CLASSPATH"
```

Then run the tool. For example
./JimpleToPDSolver -f dataflow.out "<examples.Dataflow: void main(java.lang.String[])>"

The specified method is the initial method of the program. This must be
a static method. The file `dataflow.out`

now contains a list
of pushdown rules, and a list of proposition assignments as described
above.
Rules:
csinit # -> csq cpLinit0016 #;
csq cpLinit0016 -> csq cpL_examples_Dataflow__main_ALjava_lang_String_V__11_0;
. . .
Propositions:
csq # csq #;
csq cpL_examples_Dataflow__b_V__23_12 csq cpL_examples_Dataflow__b_V__23_12 use__examples_Dataflow__int_i_ def__i1__in___examples_Dataflow__b_V_;
. . .

```
The initial configuration of the program is
``````
<csinit,
#>
```

. The main control state is `csq`

and
`csend`

is reached when the program terminates. The alphabet
contains labels of the form
cpL_<class>__<method name>__<argument types>__<line no>_<unique id>

The following propositions are assigned to each control state and stack
character pair:
- the name of the control state,
- the name of the stack character,
`use__<var name>__in___<method info>`

for any variables used (but not modified) by the program line.
Note that the method information is only present in local
variables, and specifies which method the variable is local
to,
`def__<var name>__in___<method info>`

for any variables defined (but not used) by the program line,
and
`usedef__<var name>__in___<method info>`

for any variables both used and defined by the program line.

The generated file can be turned into a `pdmu`

file with the
addition of a `Mu Property`

section.
#### Translation Strategy

JimpleToPDSolver translates the Jimple representation of the program
to a pushdown system. Each statement roughly corresponds to one Jimple
command. All data values are ignored, so statements such as assignments
simply move to the next control point, while conditional statements
branch non-deterministically to any of the possible successor points.
Virtual method calls are resolved by adding a branch calling each of
the implementing methods present in the program (that is, in any class
mentioned in the code).

When an exception is thrown, if its type can be determined
statically, execution branches to the appropriate catch block, if one
occurs. Otherwise the current method returns. If the type cannot be
determined, we branch to any of the available catch blocks, or
return. At each return point there is a branch that assumes an
exception could have been returned. Hence, as well as continuing
execution, we may also branch to any available catch blocks, or return
from the method.

## Change Log

- 29th October 2010:
- Several minor fixes to input and output processing: infers alphabet from
interesting configurations as well as pds rules; removes fixed
points of atomic formulas; detects unbound variables in input
formula; output initial and final states of automaton. [pdsolver-1.1.1.tgz]
- 28th October 2010:
- Added 'Interesting Configurations' feature. [pdsolver-1.1.0.tgz]
- Earlier:
- Original release. [pdsolver-1.0.0.tgz]

## References

- [Concur09]
- M. Hague and C.-H. L. Ong.
Winning regions of
pushdown parity games: A saturation method . In CONCUR 2009, pages
384–398.
[pdf]
- [I&C10]
- M. Hague and C.-H. L. Ong.
A Saturation Method for the Modal
Mu-Calculus over Pushdown Systems. Inf. Comput. 209(5): 799-821 (2011) 2010.
[pdf]
- [Backwards10]
- M. Hague and C.-H. L. Ong.
A
saturation method for the modal mu- calculus with backwards modalities
over pushdown systems , 2010.
[pdf]
- [Spin10]
- M. Hague and C.-H. L. Ong.
Analysing
Mu-Calculus Properties of Pushdown Systems .
In SPIN, 2010. [pdf]