Browse Source

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
master
Dave Parker 15 years ago
parent
commit
ebf163a14e
  1. 7
      prism/src/pta/DBM.java
  2. 6
      prism/src/pta/DBMList.java

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

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

Loading…
Cancel
Save