In addition to declaring some variables to be observable using an
observables ... endobservables block, other observables can be
defined as follows:
observable "top" = y=ymax;
which comprises a name and an expression to define it.
These named observables can appear in properties (e.g., to express
a target for reachability) in the same way as labels.
The ModelGenerator/ModelInfo interfaces are updated accordingly.
The key methods that need to be implemented are getObservableNames()
and getObservableTypes(), in ModelInfo and getObservation(State),
in ModelGenerator. As an optimisation (but essential for efficiency
in practice) isVarObservable() should also be implemented, since this
is needed to construct Belief objects that are as compact as possible.
Implementation/code details:
* New parser AST classes: ObservableVars/Observable (for observable
definitions in ModulesFile) and ExpressionObs (for references to
observables in expressions).
* A few imports are fixed to avoid names clases with Observable
* Observations/unobservations are now just stored as State objects,
so the Observation/Unobservation classes (in parser) are now redundant
and have been removed.
This sets the working directory natively, which is used to read or
write files specified with relative locations. For example:
prism -dir /some/dir model.prism model.props
is the same as:
prism /some/dir/model.prism /some/dir/model.props
Exported files also go to the same directory.
The same applies when passing model/property files to the GUI via
the command-line and when specifying export filenames as options.
The GUI file chooser is also initialised to the -dir location.
Calling code should be calling Prism.setPRISMModelConstants now,
after recent changes to the usage of Prism. But the methods
in GUISimulator got missed when this was updated elsewhere.
This allows simulation and statistical model checking to be performed on
a wider range of model sources, not just PRISM language models.
SimulatorEngine and associated files have had their dependencies on
ModulesFile removed, now using ModelGenerator and RewardGenerator
instead. SimulatorEngine also no longer uses TransitionList and Updater:
these are internal to the ModulesFileModelGenerator which provides
ModelGenerator access to a PRISM model.
Associated simulator classes have been altered too. Path and Sampler
classes now use a ModelInfo and RewardGenerator, rather than a
ModulesFile and TransitionList. Path classes store an action object and
action string, rather than action info specific to a ModulesFile. This
means that the methods getTransitionModuleOrAction and
getTransitionModuleOrActionIndex disappear from SimulatorEngine,replaced
by getTransitionAction and getTransitionActionString.
Usage of SimulatorEngine changes slightly. There is now a loadModel()
method, after which paths are created or statistical model checking
initiated, rather than a ModulesFile being passed to these latter
methods as done previously. The main function of SimulatorEngine is
manual/automatic path creation and statistical model checking. Exploring
states/transitions of a model is now de-emphasised, since this is
already provided directly by the passed in ModelGenerator. But
SimulatorEngine still provide access to information about transitions
etc. in the model because it allows this to be queried for arbitrary
states along created paths. The method checkModelForSimulation() has
been removed - since these checks now occur earlier at the point of
creating a ModelGenerator - and is now in Prism instead.
In Prism, in line with other recent changes, simulation-based methods
now use the currently loaded model, rather than taking a passed in
ModulesFile. For use within these methods, or from other methods that
want to access SimulatorEngine directly, there is a new method
loadModelIntoSimulator().
A model is needed for context (i.e., for access to variables, constants, labels, etc.).
Previous methods required the user to pass in a ModelInfo object for this purpose.
These new methods should now be preferred to the old ones.
Calls have been replaced where possible, including a slight reorder of parsing/loading in PrismCL.
In the GUI, the parsed model is cached locally in various places but should always
be the same as the one currently loaded into PRISM.
This is part of an ongoing effort to reduce the extent to which code is
tied to the PRISM language (i.e., ModulesFile) specifically.,
and to push make the Prism object more generally useful as an API.
Export the values of the following standard compiler and compiler flag
variables in the main makefile, avoiding the need to pass through each
one to child make processes manually:
CC
CXX
LD
JAVAC
JAVACC
Since JAVAC is manually exported as "$(JAVAC) $(JFLAGS)" by the main
makefile, additionally separate JAVAC and JFLAGS into separate variables
from the perspective of child make processes.
Rename the following makefile variables for the sake of clarity in child
makefiles:
SRC_DIR -> PRISM_SRC_DIR
CLASSES_DIR -> PRISM_CLASSES_DIR
OBJ_DIR -> PRISM_OBJ_DIR
LIB_DIR -> PRISM_LIB_DIR
INCLUDE_DIR -> PRISM_INCLUDE_DIR
IMAGES_DIR -> PRISM_IMAGES_DIR
DTDS_DIR -> PRISM_DTDS_DIR
The helper script src/scripts/printversion.sh also makes use of the
value of SRC_DIR exported from the main makefile, so use PRISM_SRC_DIR
in that script too.
Previously, during the constructor of GUIMultiModelHandler, a WaitParseThread
was created. If the startup of the other plugins takes longer than the configured delay
(default = 1s, but can be much shorter via settings), the attempted parse can generate
events that reach other plugins/components that are not yet fully initialised, leading
to NullPointerExceptions, etc.
Now, we inhibit the creation of the WaitParseThread until the startup has
completed.
Fixes#111.
For 'Export path' from the simulator in the GUI:
If there are reward structures in the model, ask the user whether the
exported path should include the reward information as well.
Indicate in the "Method" part of the result in the GUI that
nondeterminism in the model was resolved uniformly by the
statistical model checking engine.
We have observed crashes during GUI startup, during the splash screen phase, with the following exception stack trace:
Exception in thread "main" java.util.ConcurrentModificationException
at java.util.Vector$Itr.checkForComodification(Vector.java:1184)
at java.util.Vector$Itr.next(Vector.java:1137)
at javax.swing.plaf.basic.BasicDirectoryModel$LoadFilesThread.cancelRunnables(BasicDirectoryModel.java:340)
at javax.swing.plaf.basic.BasicDirectoryModel$LoadFilesThread.cancelRunnables(BasicDirectoryModel.java:346)
at javax.swing.plaf.basic.BasicDirectoryModel.validateFileCache(BasicDirectoryModel.java:135)
at javax.swing.plaf.basic.BasicDirectoryModel.propertyChange(BasicDirectoryModel.java:69)
at java.beans.PropertyChangeSupport.fire(PropertyChangeSupport.java:335)
at java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:327)
at java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:263)
at java.awt.Component.firePropertyChange(Component.java:8422)
at javax.swing.JFileChooser.setCurrentDirectory(JFileChooser.java:598)
at userinterface.GUIPrism.setupResources(GUIPrism.java:262)
at userinterface.GUIPrism.<init>(GUIPrism.java:228)
at userinterface.GUIPrism.main(GUIPrism.java:127)
The problem seems to be that creating a JFileChooser and then using setCurrentDirectory a short time later might result in some race condition in the Java platform code (the JFileChooser asynchronously pre-caches the directory contents and has to cancel these threads when the directory is changed). We have also not been able to reliably trigger it.
While this doesn't look to be our fault, we avoid this by doing the currentDir logic before creating the JFileChooser and then passing this directly during the construction of the JFileChooser.
(with Philipp Chrszon)
(1) In general, for user actions (a_...), ensure that setComputing(false)
is called even if the underlying computing resulted in an exception.
This ensures that the buttons/menu items of the simulator are properly
enabled again and we don't get into a deadlock situation where we
can't even start a new path.
(2) For the automatic step actions, ensure that the path display is
updated even if there is an exception, as there may have been
intermediate steps that had succeeded before the error occurred.
Previously, the resulting distance was considered as a time value,
not a step value. For discrete time models, this coincidently does
the right thing, but for continuous time models this does not work as expected.
Technically, as engine.getPathSize() is a long and the value from the text box
is an int, the result is a long and that leads Java to prefer the a_backTrack(double)
and a_autoStep(double) variants of these methods. We cast to an int to ensure
that the int-parameter variants are taken.
As noted in #68, the javah tool has been removed in JDK10. Here, we switch to the new way of generating the JNI .h files, using the -h option of the regular javac compiler.
We have to adapt all Makefiles (not only those in directories that contain classes with native methods), as javac compiles all required classes (and generates their JNI headers) beyond the directory with the Makefile.
The .h files generated by javac -h had a different naming scheme, now there is a prefix for the package name. To avoid having to touch all the #includes, we generate the new .h files in prism/include/jni and provide legacy headers in the old location and with the old name, forwarding the the corresponding new header. In the future, at an appropriate moment, those legacy headers can be removed and replace with direct includes.
Currently, there is a post-processing step on Windows: After the .h file is generated, dos2unix is called to replace the Windows CRLF line endings. Otherwise, the generated headers show up as changed files in version control. As now there are no special targets for the generation of the .h files anymore, we move to a global post-processing step and call dos2unix on prism/include/jni/*.h at the end of building.
Similar to the behaviour in the properties list, if we double-click
inside the constant or label table but not on an existing entry, we
add a new contant/label line in the table.
Using the infrastructure from the previous commit, we request exact evaluation
of constants in exact and parametric model checking mode.
Additionally, note where we deliberately choose non-exact evaluation mode.
Add corresponding test cases.
In Java 9, there is a new system class java.lang.Module that is implicitly imported
everywhere and which clashes with the parser.ast.Module class, resulting in
compilation errors, as javac is not able to disambiguate between the two
automatically.
We are therefore more specific when referencing the PRISM parser's 'Module' class,
by using the full 'parser.ast.Module' name.
Currently, building PRISM with parallel building does not work,
as there are dependencies between targets that are not fully
encoded in the Makefiles. Building with -j n flag would lead to error.
Now, we add the .NOTPARALLEL target to most of the Makefiles,
which tell GNU make to ignore the -j flag. Note that this
only inhibits parallel builds for the current Makefile, we
thus have to specify it for all sub-Makefiles as well
(see https://www.gnu.org/software/make/manual/html_node/Parallel.html)
For the external libraries, CUDD and LPSolve don't seem to mind building
in parallel, so we don't inhibit there and can get some minor compile time
speed-up by using multiple cores if the -j option is specified.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12202 bbc10eb1-c90d-0410-af57-cb519fbb1720
Currently, properties that contain an undefined property constant are not displayed.
In the future it might be nice for the user to be asked to specify these constants,
preferably in an unobstrusive way, so that these path formulae can be displayed and
evaluated as well.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11444 bbc10eb1-c90d-0410-af57-cb519fbb1720
Now, double-clicking on a property will open the editor
for that property. Double-clicking on an empty area of the
property list will open the "new property" editor.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11109 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein