diff --git a/prism/Makefile b/prism/Makefile index 386506fb..feee0c43 100644 --- a/prism/Makefile +++ b/prism/Makefile @@ -437,7 +437,7 @@ tarcf: PRISM_CLASSPATH = "$(CLASSES_DIR)$(CLASSPATHSEP)$(LIB_DIR)/jcommon.jar$(CLASSPATHSEP)$(LIB_DIR)/jfreechart.jar$(CLASSPATHSEP)$(LIB_DIR)/epsgraphics.jar$(CLASSPATHSEP)$(LIB_DIR)/colt.jar" javadoc: - @JAVADOC_DIRS=`echo $(MAKE_DIRS) | sed 's/\//./g' | sed 's/ /:/g'` && \mkdir -p javadoc; javadoc -d javadoc -classpath $(SRC_DIR)$(CLASSPATHSEP)$(PRISM_CLASSPATH) -subpackages $$JAVADOC_DIRS + @JAVADOC_DIRS=`echo $(MAKE_DIRS) | sed 's/\//./g' | sed 's/ /:/g'` && \mkdir -p javadoc; javadoc -d javadoc -overview $(SRC_DIR)/overview.html -sourcepath $(SRC_DIR) -classpath $(SRC_DIR)$(CLASSPATHSEP)$(PRISM_CLASSPATH) -subpackages $$JAVADOC_DIRS clean: checks @(for dir in $(MAKE_DIRS); do \ diff --git a/prism/src/dv/package-info.java b/prism/src/dv/package-info.java new file mode 100644 index 00000000..64fe5050 --- /dev/null +++ b/prism/src/dv/package-info.java @@ -0,0 +1,4 @@ +/** + * Utility functions for operations on vectors of doubles (stored in C++ through JNI). + */ +package dv; diff --git a/prism/src/explicit/package-info.java b/prism/src/explicit/package-info.java new file mode 100644 index 00000000..b5d74510 --- /dev/null +++ b/prism/src/explicit/package-info.java @@ -0,0 +1,4 @@ +/** + * Explicit-state probabilistic model checking engine, implemented in Java, and quantitative abstraction refinement techniques (see {@link explicit.QuantAbstractRefine}). + */ +package explicit; diff --git a/prism/src/hybrid/package-info.java b/prism/src/hybrid/package-info.java new file mode 100644 index 00000000..2d3cf921 --- /dev/null +++ b/prism/src/hybrid/package-info.java @@ -0,0 +1,4 @@ +/** + * Access to the "Hybrid" engine: data structures and model checking algorithms that mix MTBDDs and explicit-state techniques. + */ +package hybrid; diff --git a/prism/src/jdd/package-info.java b/prism/src/jdd/package-info.java new file mode 100644 index 00000000..fc7673f9 --- /dev/null +++ b/prism/src/jdd/package-info.java @@ -0,0 +1,4 @@ +/** + * A Java library providing a wrapper around the dd library and hence Java access to CUDD via JNI. + */ +package jdd; diff --git a/prism/src/jltl2ba/package-info.java b/prism/src/jltl2ba/package-info.java new file mode 100644 index 00000000..0e4e60d3 --- /dev/null +++ b/prism/src/jltl2ba/package-info.java @@ -0,0 +1,4 @@ +/** + * Java port of the LTL to Buchi automata conversion library. + */ +package jltl2ba; diff --git a/prism/src/jltl2dstar/package-info.java b/prism/src/jltl2dstar/package-info.java new file mode 100644 index 00000000..d35f151c --- /dev/null +++ b/prism/src/jltl2dstar/package-info.java @@ -0,0 +1,4 @@ +/** + * Java port of the LTL to deterministic Rabin automata conversion library. + */ +package jltl2dstar; diff --git a/prism/src/mtbdd/package-info.java b/prism/src/mtbdd/package-info.java new file mode 100644 index 00000000..7089cef2 --- /dev/null +++ b/prism/src/mtbdd/package-info.java @@ -0,0 +1,4 @@ +/** + * Access to the "MTBDD" engine: fully symbolic implementations of model checking algorithms. + */ +package mtbdd; diff --git a/prism/src/odd/package-info.java b/prism/src/odd/package-info.java new file mode 100644 index 00000000..a067488e --- /dev/null +++ b/prism/src/odd/package-info.java @@ -0,0 +1,4 @@ +/** + * Access to ODDs (offset-labelled BDDs), used to facilitate indexing of states between BDDs and explicit-state data structures. + */ +package odd; diff --git a/prism/src/overview.html b/prism/src/overview.html new file mode 100644 index 00000000..1a2e5cf0 --- /dev/null +++ b/prism/src/overview.html @@ -0,0 +1,3 @@ + +This is the documentation for PRISM's Java code: for the discrete-event simulation engine, see {@link simulator.SimulatorEngine}; for the explicit-state probabilistic model checking and abstraction-refinement, see package {@link explicit}. + diff --git a/prism/src/parser/ast/package-info.java b/prism/src/parser/ast/package-info.java new file mode 100644 index 00000000..d413d447 --- /dev/null +++ b/prism/src/parser/ast/package-info.java @@ -0,0 +1,4 @@ +/** + * Abstract syntax tree data structures for the PRISM model/properties parser. + */ +package parser.ast; diff --git a/prism/src/parser/package-info.java b/prism/src/parser/package-info.java new file mode 100644 index 00000000..41e42a63 --- /dev/null +++ b/prism/src/parser/package-info.java @@ -0,0 +1,4 @@ +/** + * The PRISM model/properties parser, accompanying abstract syntax tree data structures and tools (including JavaCC-generated code). + */ +package parser; diff --git a/prism/src/parser/type/package-info.java b/prism/src/parser/type/package-info.java new file mode 100644 index 00000000..e3dbd17d --- /dev/null +++ b/prism/src/parser/type/package-info.java @@ -0,0 +1,4 @@ +/** + * Type system for the PRISM model/properties parser. + */ +package parser.type; diff --git a/prism/src/parser/visitor/package-info.java b/prism/src/parser/visitor/package-info.java new file mode 100644 index 00000000..d6f83979 --- /dev/null +++ b/prism/src/parser/visitor/package-info.java @@ -0,0 +1,4 @@ +/** + * Syntax tree traversal operations for the PRISM model/properties parser (implemented with the "visitor" pattern). + */ +package parser.visitor; diff --git a/prism/src/pepa/compiler/package-info.java b/prism/src/pepa/compiler/package-info.java new file mode 100644 index 00000000..e44d3e4c --- /dev/null +++ b/prism/src/pepa/compiler/package-info.java @@ -0,0 +1,4 @@ +/** + * Access to PEPA-to-PRISM model translation. + */ +package pepa.compiler; diff --git a/prism/src/prism/package-info.java b/prism/src/prism/package-info.java new file mode 100644 index 00000000..c8a007a5 --- /dev/null +++ b/prism/src/prism/package-info.java @@ -0,0 +1,6 @@ +/** + * The main Prism API, the command-line tool, and Java classes for symbolic data structures and algorithms. + * + * See {@link prism.Prism} for details. + */ +package prism; diff --git a/prism/src/pta/package-info.java b/prism/src/pta/package-info.java new file mode 100644 index 00000000..05889f8a --- /dev/null +++ b/prism/src/pta/package-info.java @@ -0,0 +1,4 @@ +/** + * Probabilistic timed automata (PTA) model checking, including DBM library. + */ +package pta; diff --git a/prism/src/pta/parser/package-info.java b/prism/src/pta/parser/package-info.java new file mode 100644 index 00000000..cc4c8a9a --- /dev/null +++ b/prism/src/pta/parser/package-info.java @@ -0,0 +1,4 @@ +/** + * A parser for a simple PTA input language - not used in PRISM. + */ +package pta.parser; diff --git a/prism/src/settings/package-info.java b/prism/src/settings/package-info.java new file mode 100644 index 00000000..83a776cc --- /dev/null +++ b/prism/src/settings/package-info.java @@ -0,0 +1,4 @@ +/** + * Generic 'settings' functionality. + */ +package settings; diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index e6cba923..af267ae6 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -37,6 +37,8 @@ import parser.type.*; import prism.*; /** + * A discrete event simulation engine for PRISM models. + * * The SimulatorEngine class provides support for: * * - * To see the transitions available in the current state, use: - * - * - * For path manipulation... - * - * - * ... - * TODO - * * For sampling-based approximate model checking, use: *