← Back to branch summary

~ubuntu-branches/ubuntu/utopic/tcm/utopic

« back to all changes in this revision

Viewing changes to src/sd/bv/adscks.h

  • Committer: Bazaar Package Importer
  • Author(s): Otavio Salvador
  • Date: 2003-07-03 20:08:21 UTC
  • Revision ID: james.westby@ubuntu.com-20030703200821-se4xtqx25e5miczi
Tags: upstream-2.20
Import upstream version 2.20

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/sd/bv/adscks.h
 
1
//////////////////////////////////////////////////////////////////////////////////
 
2
// This file is part of Toolkit for Conceptual Modeling (TCM).
 
3
// (c) copyright 2001, Universiteit Twente.
 
4
// Author: Rik Eshuis (eshuis@cs.utwente.nl).
 
5
//
 
6
// TCM is free software; you can redistribute it and/or modify
 
7
// it under the terms of the GNU General Public License as published by
 
8
// the Free Software Foundation; either version 2 of the License, or
 
9
// (at your option) any later version.
 
10
//
 
11
// TCM is distributed in the hope that it will be useful,
 
12
// but WITHOUT ANY WARRANTY; without even the implied warranty of
 
13
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
14
// GNU General Public License for more details.
 
15
//
 
16
// You should have received a copy of the GNU General Public License
 
17
// along with TCM; if not, write to the Free Software
 
18
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 
19
// 02111-1307, USA.
 
20
////////////////////////////////////////////////////////////////////////////////
 
21
#ifndef _ADSCKS_H
 
22
#define _ADSCKS_H
 
23
 
 
24
#include "llist.h"
 
25
//#include "point.h"
 
26
//#include "lstring.h"
 
27
//class Node;
 
28
//class AdKTransition;
 
29
//class Subject;
 
30
//class OutputFile;
 
31
//#include "node.h"
 
32
//#include "AdKtransition.h"
 
33
//#include "AdKlocation.h"
 
34
#include "graph.h"
 
35
#include "bool.h"
 
36
#include "hashlist.h"
 
37
//#include "adshypergraph.h"
 
38
 
 
39
class ClockManager;
 
40
class ADSValuation;
 
41
class ADSTransition;
 
42
class ADSHyperGraph;
 
43
 
 
44
///  class CKS, consisting of valuations and transitions
 
45
class ADSCks :public Graph {
 
46
/*@Doc: {\large {\bf scope:} diagram} */
 
47
public:
 
48
        ///
 
49
        ADSCks(ADSHyperGraph *a); 
 
50
        ///
 
51
        ~ADSCks();
 
52
        ///
 
53
        void AddNode(Node *);
 
54
        ///
 
55
        void AddEdge(Edge *);
 
56
        ///
 
57
        void InitConnections(){};
 
58
        ///
 
59
        void WriteSubjects(OutputFile *f);
 
60
        ///
 
61
        void WriteSMVFile(OutputFile *f, bool tlv);
 
62
        ///
 
63
        //bool ExistsSimilarNode( ADSValuation *s);
 
64
        ///
 
65
        bool ExistsSimilarEdge( ADSTransition *s);
 
66
        /// 
 
67
        ADSValuation *FindSimilarNode( ADSValuation *s);
 
68
        /// checks whether the configuration in valuation s has become unbounded
 
69
        /// using a check from the Karp Miller algorithm for Petri nets
 
70
        bool GrowsInfinite(ADSValuation *s, string &str);
 
71
        ///
 
72
        void GetClocks(List <string> *l);
 
73
        /// generate index number for valuations
 
74
        void AssignNumbers();
 
75
        /// 
 
76
        ADSHyperGraph *GetADSHyperGraph(){return am;};
 
77
        /// get valuation with index i
 
78
        ADSValuation *GetADSValuation(int i);
 
79
        ///
 
80
        int countconfigs();
 
81
 
 
82
 private:
 
83
        /// the original activity hypergraph
 
84
        ADSHyperGraph *am; 
 
85
        ///
 
86
        //      ValuationHashList vhl;
 
87
        ///
 
88
        //      TransitionHashList thl;
 
89
        
 
90
 
 
91
};
 
92
#endif