|
|
|
@ -26,24 +26,52 @@ |
|
|
|
|
|
|
|
package prism; |
|
|
|
|
|
|
|
import java.io.*; |
|
|
|
import java.util.*; |
|
|
|
|
|
|
|
import jdd.*; |
|
|
|
import dv.*; |
|
|
|
import explicit.*; |
|
|
|
import odd.*; |
|
|
|
import mtbdd.*; |
|
|
|
import sparse.*; |
|
|
|
import hybrid.*; |
|
|
|
import hybrid.PrismHybrid; |
|
|
|
|
|
|
|
import java.io.ByteArrayInputStream; |
|
|
|
import java.io.File; |
|
|
|
import java.io.FileInputStream; |
|
|
|
import java.io.FileNotFoundException; |
|
|
|
import java.io.FileWriter; |
|
|
|
import java.io.IOException; |
|
|
|
import java.util.ArrayList; |
|
|
|
import java.util.List; |
|
|
|
import java.util.Vector; |
|
|
|
|
|
|
|
import jdd.JDD; |
|
|
|
import jdd.JDDNode; |
|
|
|
import jdd.JDDVars; |
|
|
|
import mtbdd.PrismMTBDD; |
|
|
|
import odd.ODDUtils; |
|
|
|
import param.ModelBuilder; |
|
|
|
import param.ParamModelChecker; |
|
|
|
import parser.*; |
|
|
|
import parser.ast.*; |
|
|
|
import simulator.*; |
|
|
|
import parser.ExplicitFiles2ModulesFile; |
|
|
|
import parser.PrismParser; |
|
|
|
import parser.State; |
|
|
|
import parser.Values; |
|
|
|
import parser.ast.ConstantList; |
|
|
|
import parser.ast.Expression; |
|
|
|
import parser.ast.ForLoop; |
|
|
|
import parser.ast.FormulaList; |
|
|
|
import parser.ast.LabelList; |
|
|
|
import parser.ast.ModulesFile; |
|
|
|
import parser.ast.PropertiesFile; |
|
|
|
import parser.ast.Property; |
|
|
|
import pta.DigitalClocks; |
|
|
|
import pta.PTAModelChecker; |
|
|
|
import simulator.GenerateSimulationPath; |
|
|
|
import simulator.PrismModelExplorer; |
|
|
|
import simulator.SimulatorEngine; |
|
|
|
import simulator.method.SimulationMethod; |
|
|
|
import pta.*; |
|
|
|
import prism.Model; |
|
|
|
import sparse.PrismSparse; |
|
|
|
import dv.DoubleVector; |
|
|
|
import explicit.CTMC; |
|
|
|
import explicit.CTMCModelChecker; |
|
|
|
import explicit.ConstructModel; |
|
|
|
import explicit.DTMC; |
|
|
|
import explicit.DTMCModelChecker; |
|
|
|
import explicit.FastAdaptiveUniformisation; |
|
|
|
import explicit.FastAdaptiveUniformisationModelChecker; |
|
|
|
|
|
|
|
/** |
|
|
|
* Main class for all PRISM's core functionality. |
|
|
|
|