Removed unnecessary svn:ignore (these are handles in global svn config).

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

prism/NOTES

@@ -8,9 +8,9 @@ TODO (before any release)
 -------------------------
 
 PTAs:
+* Implement divergence fix
+* Sort out "time-lock" error message
 * (Further) tidy of prism-examples/pta
-* Clarify time divergence issues
-* non-zeno checks?
 
 =======================================================
 
@@ -26,6 +26,9 @@ Filters, property semantics, etc.
 * Restructure Result class? e.g. separate bracketed comment? (done I think)
   - Errors (Exceptions) formatted properly?
 
+Action labels:
+* Check status of export/import trans wrt actions (alll models)
+
 Sim:
 * tidy doSampling, looking at Vincent's code
 * seed issues (Vlad)
@@ -40,8 +43,12 @@ PTAs:
     (see non-well-formed.nm/pctl for a test case)
     (if can't do that, syntax check using sat)
   - digital clocks: check invariants after transform/reach?
-* Digital clocks: No time-bounded until yet
-* Digital clocks: Translation done sep for each property (e.g. for cmax)?
+    (might be like non-pta case: doing before reach causes false alarms?)
+* Digital clocks time-bounded
+  - will need to make sure cmax is updated accordingly
+    (currently just from temporal operator time bound since no clocks in formula)
+  - also might need to access property constants (see TODO in DC.java)
+
 * Bug fix: action alphabet (syntactic) for sync lost in PTA object construction
 
 DOC (before public release)
@@ -72,6 +79,7 @@ PTAs:
   - access to other local and global vars
   - system endsystem?
  (then test on Arnd's BRP model + others)
+* Implement structurally non-zeno checks
 * BRP example
 * Translate non-convex guards to DNF and multiple transitions
 * Investigate whether non-convex invariants can be supported (look at zone ops)

prism/NOTES-PTAS.txt

@@ -9,6 +9,8 @@ In guards or invariants, references to clocks must be conjunctions of simple clo
 
 There are also some additional restrictions for PTA models. Modules cannot read the local variables of other modules and global variables are not permitted. The model must also have a single initial state (i.e. the init...endinit construct is not permitted). Again, when using digital clocks, the latter constraint does not apply.
 
+Model checking requires several assumptions: we require PTAs to be well-formed and non-zeno (see e.g. [KNP09c] for details). Currently, PRISM does not check automatically that these assumptions are satisfied.
+
 There are a set of PRISM PTA examples in the directory examples/pta. See the formats09.sh script in this directory for details of how to run the examples.
 
 * Properties

prism/src/pta/ForwardsReach.java

@@ -97,7 +97,8 @@ public class ForwardsReach
 		IndexedSet<LocZone> Yset;
 		//LocZoneSetOld Zset;
 		ReachabilityGraph graph;
-		int src, dest, count;
+		int src, dest, count, dests[];
+		boolean canDiverge;
 		long timer, timerProgress;
 		boolean progressDisplayed;
 
@@ -138,24 +139,34 @@ public class ForwardsReach
 			// Compute timed post for this zone (NB: do this before checking if target)
 			lz = lz.deepCopy();
 			lz.tPost(pta);
-			// Is this a target state?
+			// Is this a target state? (If so, don't explore)
 			if (targetLocs.get(lz.loc) && (targetConstraint == null || lz.zone.isSatisfied(targetConstraint))) {
 				target.set(src);
 				// Add null for this state (no need to store info)
 				graph.addState();
 				continue;
 			}
-			// Otherwise, explore this symbolic state
-			// First, check there is at least one transition
-			// (don't want deadlocks in non-target states)
-			if (pta.getTransitions(lz.loc).size() == 0) {
-				throw new PrismException("Deadlock (no transitions) in PTA at location \"" + pta.getLocationNameString(lz.loc) + "\"");
+			// Check if time can diverge in this state
+			canDiverge = lz.zone.allClocksAreUnbounded();
+			// Explore this symbolic state
+			// First, check for possibility of timelock: if there are no PTA transitions
+			// and it is not possible for time to diverge in this state
+			if (!canDiverge && pta.getTransitions(lz.loc).size() == 0) {
+				throw new PrismException("Timelock (no transitions) in PTA at location \"" + pta.getLocationNameString(lz.loc) + "\"");
 			}
 			// Add current state to reachability graph
 			graph.addState();
+			// For unbounded case, add a special self-loop transition to model divergence
+			if (canDiverge) {
+				dests = new int[1];
+				dests[0] = src;
+				Transition trNew = new Transition(pta, src, "_diverge");
+				trNew.addEdge(1.0, src);
+				graph.addTransition(src, trNew, dests, null);
+			}
 			// For each outgoing transition...
 			for (Transition transition : pta.getTransitions(lz.loc)) {
-				int[] dests = new int[transition.getNumEdges()];
+				dests = new int[transition.getNumEdges()];
 				boolean enabled = false;
 				boolean unenabled = false;
 				count = 0;