From ebf163a14e021068ac24c1c27f7fe5fd2669aab3 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 2 Aug 2011 12:26:15 +0000
Subject: [PATCH] Code doc: Added some useful references to DBM classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3348 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/DBM.java     | 7 +++++++
 prism/src/pta/DBMList.java | 6 ++++++
 2 files changed, 13 insertions(+)

diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java
index fa4139de..bf7381be 100644
--- a/prism/src/pta/DBM.java
+++ b/prism/src/pta/DBM.java
@@ -26,6 +26,13 @@
 
 package pta;
 
+/**
+ * Implementation of the difference-bound matrix (DBM) data structure.
+ * 
+ * Data structures and algorithms are mostly based on those from: 
+ * Johan Bengtsson, Wang Yi: Timed Automata: Semantics, Algorithms and Tools.
+ * Lectures on Concurrency and Petri Nets 2003, LNCS volume 3098, pages 87-124, Springer, 2004
+ */
 public class DBM extends Zone
 {
 	/* Parent PTA */
diff --git a/prism/src/pta/DBMList.java b/prism/src/pta/DBMList.java
index db70d366..ec7eacf5 100644
--- a/prism/src/pta/DBMList.java
+++ b/prism/src/pta/DBMList.java
@@ -28,6 +28,12 @@ package pta;
 
 import java.util.*;
 
+/**
+ * List of DBMs representing a non-convex zone.
+ * 
+ * See this reference for some useful algorithms:
+ * S. Tripakis. The formal analysis of timed systems in practice. Joseph Fourier University, 1998.
+ */
 public class DBMList extends NCZone
 {
 	/* Parent PTA */