Improved documentation (JavaDoc mostly).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2436 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago · 35f377ab3e
37 changed files with 144 additions and 14 deletions
--- 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 \
--- a/prism/src/dv/package-info.java
+++ 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;
--- a/prism/src/explicit/package-info.java
+++ 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;
--- a/prism/src/hybrid/package-info.java
+++ 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;
--- a/prism/src/jdd/package-info.java
+++ 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;
--- a/prism/src/jltl2ba/package-info.java
+++ b/prism/src/jltl2ba/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Java port of the LTL to Buchi automata conversion library.
+ */
+package jltl2ba;
--- a/prism/src/jltl2dstar/package-info.java
+++ b/prism/src/jltl2dstar/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Java port of the LTL to deterministic Rabin automata conversion library.
+ */
+package jltl2dstar;
--- a/prism/src/mtbdd/package-info.java
+++ 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;
--- a/prism/src/odd/package-info.java
+++ 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;
--- a/prism/src/overview.html
+++ b/prism/src/overview.html
@ -0,0 +1,3 @@
+<html><head></head><body>
+This is the documentation for <a href="http://www.prismmodelchecker.org/">PRISM<a>'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}.
+</body></html>
--- a/prism/src/parser/ast/package-info.java
+++ 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;
--- a/prism/src/parser/package-info.java
+++ 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;
--- a/prism/src/parser/type/package-info.java
+++ b/prism/src/parser/type/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Type system for the PRISM model/properties parser.
+ */
+package parser.type;
--- a/prism/src/parser/visitor/package-info.java
+++ 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;
--- a/prism/src/pepa/compiler/package-info.java
+++ b/prism/src/pepa/compiler/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Access to PEPA-to-PRISM model translation.
+ */
+package pepa.compiler;
--- a/prism/src/prism/package-info.java
+++ 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;
--- a/prism/src/pta/package-info.java
+++ b/prism/src/pta/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Probabilistic timed automata (PTA) model checking, including DBM library.
+ */
+package pta;
--- a/prism/src/pta/parser/package-info.java
+++ 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;
--- a/prism/src/settings/package-info.java
+++ b/prism/src/settings/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Generic 'settings' functionality.
+ */
+package settings;
--- 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:
 * <UL>
 * <LI> State/model exploration
@ -63,19 +65,6 @@ import prism.*;
 * <LI> {@link #initialisePath}
 * </UL>
 * 
- * To see the transitions available in the current state, use:
- * <UL>
- * <LI> ... TODO
- * </UL>
- * 
- * For path manipulation...
- * <UL>
- * <LI> ... TODO
- * </UL>
- * 
- * ...
- * TODO
- * 
 * For sampling-based approximate model checking, use:
 * <UL>
 * <LI> {@link #checkPropertyForSimulation}
--- a/prism/src/simulator/method/package-info.java
+++ b/prism/src/simulator/method/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Implementation of approximate/statistical model checking techniques using the discrete event simulation engine.
+ */
+package simulator.method;
--- a/prism/src/simulator/networking/package-info.java
+++ b/prism/src/simulator/networking/package-info.java
@ -0,0 +1,4 @@
+/**
+ * (not used)
+ */
+package simulator.networking;
--- a/prism/src/simulator/package-info.java
+++ b/prism/src/simulator/package-info.java
@ -0,0 +1,4 @@
+/**
+ * The discrete event simulation engine and approximate (statistical) model checking code.
+ */
+package simulator;
--- a/prism/src/simulator/sampler/package-info.java
+++ b/prism/src/simulator/sampler/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Code for checking properties against simulation paths generated by discrete event simulation engine.
+ */
+package simulator.sampler;
--- a/prism/src/sparse/package-info.java
+++ b/prism/src/sparse/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Access to the "Sparse" engine: sparse matrix data structures and corresponding implementations of model checking algorithms.
+ */
+package sparse;
--- a/prism/src/userinterface/graph/package-info.java
+++ b/prism/src/userinterface/graph/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Graph plotting/editing functionality used in the GUI.
+ */
+package userinterface.graph;
--- a/prism/src/userinterface/log/package-info.java
+++ b/prism/src/userinterface/log/package-info.java
@ -0,0 +1,4 @@
+/**
+ * The "Log" tab in the GUI.
+ */
+package userinterface.log;
--- a/prism/src/userinterface/model/computation/package-info.java
+++ b/prism/src/userinterface/model/computation/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Computation threads for model construction functionality in the GUI ("Model" tab)
+ */
+package userinterface.model.computation;
--- a/prism/src/userinterface/model/graphicModel/package-info.java
+++ b/prism/src/userinterface/model/graphicModel/package-info.java
@ -0,0 +1,4 @@
+/**
+ * (not used)
+ */
+package userinterface.model.graphicModel;
--- a/prism/src/userinterface/model/package-info.java
+++ b/prism/src/userinterface/model/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Model editing/construction functionality in the GUI ("Model" tab)
+ */
+package userinterface.model;
--- a/prism/src/userinterface/model/pepaModel/package-info.java
+++ b/prism/src/userinterface/model/pepaModel/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Text editor for PEPA models in the GUI.
+ */
+package userinterface.model.pepaModel;
--- a/prism/src/userinterface/package-info.java
+++ b/prism/src/userinterface/package-info.java
@ -0,0 +1,4 @@
+/**
+ * PRISM's graphical user interface (GUI).
+ */
+package userinterface;
--- a/prism/src/userinterface/properties/computation/package-info.java
+++ b/prism/src/userinterface/properties/computation/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Computation threads for model checking functionality in the GUI ("Properties" tab)
+ */
+package userinterface.properties.computation;
--- a/prism/src/userinterface/properties/package-info.java
+++ b/prism/src/userinterface/properties/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Model checking functionality in the GUI ("Properties" tab)
+ */
+package userinterface.properties;
--- a/prism/src/userinterface/simulator/networking/package-info.java
+++ b/prism/src/userinterface/simulator/networking/package-info.java
@ -0,0 +1,4 @@
+/**
+ * (not used)
+ */
+package userinterface.simulator.networking;
--- a/prism/src/userinterface/simulator/package-info.java
+++ b/prism/src/userinterface/simulator/package-info.java
@ -0,0 +1,4 @@
+/**
+ * The user interface to the simulator supplied in the GUI.
+ */
+package userinterface.simulator;
--- a/prism/src/userinterface/util/package-info.java
+++ b/prism/src/userinterface/util/package-info.java
@ -0,0 +1,4 @@
+/**
+ * Various utility classes for the graphical user interface (GUI).
+ */
+package userinterface.util;