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 */