Introduce PSEModelExplorer, with some functionality having been delegated from PSEModelBuilder.
Add very primitive PSEFastAdaptiveUniformisation.

Features missing:
- Decomposing the parameter space.
- Cumulative prob loss instead of subtracting from 1.0.
- Support for model-checking or synthesis techniques.
- Converting into array when no states added/removed for a long time.
Turn PSEFastAdaptiveUniformisation into a final class.
An unsuccessful attempt to compute total probability loss.
Decomposition for PSE+FAU and other improvements.
Merge branch 'fau' into develop

PSE+FAU is far from complete:
- Only transient analysis is supported.  Model checking
  or synthesis techniques still cannot take advantage
  of FAU.
- Total probability loss is not reported, for I haven't
  found out how to compute it directly (i.e., not by
  subtracting from 1.0).

Furthermore, the most obvious optimisations are missing
as well:
- Transforming the StateProp representation into arrays
  (as in basic FAU) is not implemented.
- Special handling of non-parametrised transitions
  (as in basic PSE) is not implemented.

Conflicts:
	prism/src/pse/PSEModelBuilder.java
Better printing.
Yet another unsuccessful atempt to deal with total probability loss in PSE+FAU.
Merge branch 'fau' into develop
Bug in explicit engine LTL model checking (happens when there are multiple APs in the formula and ordering is different in the DRA). Reported by Manfred Jaeger.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9091 bbc10eb1-c90d-0410-af57-cb519fbb1720
Tweak debug print out of DRA - show APs too.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9092 bbc10eb1-c90d-0410-af57-cb519fbb1720
Bug fix in Dot export of DRA.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9093 bbc10eb1-c90d-0410-af57-cb519fbb1720
A jltl2ba bug fix from Joachim Klein - fixes various previously reported LTL->DRA crashes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9109 bbc10eb1-c90d-0410-af57-cb519fbb1720
bugfix fau

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9122 bbc10eb1-c90d-0410-af57-cb519fbb1720
fixed computation of lost probability to take into account probability mass intentionally destroyed

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9138 bbc10eb1-c90d-0410-af57-cb519fbb1720
Compile fix (to allow build on Java 6).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9143 bbc10eb1-c90d-0410-af57-cb519fbb1720
Improve simulation Sampler classes to handle deadlocks (in some cases). Deadlocks still not properly handled by the simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9147 bbc10eb1-c90d-0410-af57-cb519fbb1720
Another LTL-to-automaton bugfix from Joachim Klein (fix-bdfs.patch).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9151 bbc10eb1-c90d-0410-af57-cb519fbb1720
Another LTL-to-automaton bugfix from Joachim Klein (jltl2ba-fix-simplify-bstates--trivial-sccs.patch).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9152 bbc10eb1-c90d-0410-af57-cb519fbb1720
Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9153 bbc10eb1-c90d-0410-af57-cb519fbb1720