← Back to branch summary

~ubuntu-branches/ubuntu/intrepid/tcm/intrepid

« back to all changes in this revision

Viewing changes to src/sd/bv/adshypergraph.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/adshypergraph.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 _ADSHYPERGRAPH_H
 
22
#define _ADSHYPERGRAPH_H
 
23
 
 
24
 
 
25
#include "hypergraph.h"
 
26
#include "llist.h"
 
27
#include "bag.h"
 
28
#include "bool.h"
 
29
 
 
30
#define MAXACT 100
 
31
#define MAXNODE 100
 
32
 
 
33
class ADSActivity;
 
34
class ATDActionStateNode;
 
35
class Prop;
 
36
class ADSVar;
 
37
class OutputFile;
 
38
class Clock;
 
39
class ClockConstraint;
 
40
 
 
41
/// (abstract) graph class.
 
42
class ADSHyperGraph: public HyperGraph {
 
43
/*@Doc: {\large {\bf scope:} diagram} */
 
44
public:
 
45
        ///
 
46
        ADSHyperGraph(); 
 
47
        ///
 
48
        ~ADSHyperGraph();
 
49
 
 
50
        /// does a interfere with b?
 
51
        bool GetInterference(ADSActivity *a, ADSActivity *b);
 
52
        ///
 
53
        bool GetInterference(ATDActionStateNode *a1, ATDActionStateNode *a2);
 
54
        ///
 
55
        bool isConflicting(Bag <ADSHyperEdge *> *step, ADSHyperEdge *he);
 
56
        ///
 
57
        void Initialise();
 
58
        ///
 
59
        void Finalise();
 
60
        ///
 
61
        bool AddProp(Prop *p);
 
62
        ///
 
63
        bool AddVar(ADSVar *v);
 
64
        ///
 
65
        void RemoveProp(Prop *p);
 
66
 
 
67
        ///
 
68
        void GetPropList(List <Prop *> &l);
 
69
        ///
 
70
        void GetExtPropList(List <Prop *> &l);
 
71
        ///
 
72
        void GetIntPropList(List <Prop *> &l);
 
73
        ///
 
74
        void GetVarList(List <ADSVar *> &l);
 
75
        ///
 
76
        Prop *FindSimilarProp(Prop *p);
 
77
        ///
 
78
        ADSVar *FindSimilarVar(ADSVar *p);
 
79
        
 
80
        ///
 
81
        Node *FindNode(string name);
 
82
        ///
 
83
        //      ADSActivity *FindAct(string);
 
84
        ///  update the upper bound of each node  
 
85
        void UpdateBounds(Bag <Subject *> *cfg);
 
86
        ///  return the upper bound of node s
 
87
        int GetBound(Subject *s);
 
88
 
 
89
        ///
 
90
        int GetNrTimeouts(){return timeoutnumber;};
 
91
 
 
92
        ///
 
93
        void WriteSubjects(OutputFile *ofile);
 
94
        ///
 
95
        string DeadEdgesNodesConstraints();
 
96
        ///
 
97
        void SetInitialFinalNames();
 
98
        ///
 
99
        void UnSetInitialFinalNames();
 
100
        ///
 
101
        void WriteNuSMV(OutputFile *ofile, bool);
 
102
        ///
 
103
        string ComputeFinalPredicate();
 
104
        ///
 
105
        void GetFinalNodes(List <Subject *> *final);
 
106
 
 
107
        ///
 
108
        void RemoveLocalVariables(List <ADSVar *> *used);
 
109
 
 
110
        ///
 
111
        void RemoveNodes(List <Node *> , List <ADSVar *>, bool reduction);
 
112
 
 
113
 
 
114
 protected:
 
115
        ///
 
116
        void ComputeActivities();
 
117
        ///
 
118
        void ComputeConflicts();
 
119
        ///
 
120
        void ComputeInterferences();
 
121
        ///
 
122
        void ComputeInternalProperties();
 
123
        ///
 
124
        void ComputeInternalHyperEdges();
 
125
        ///
 
126
        void ComputeExternalProperties();
 
127
        /// how many timeout are there in the hypergraph
 
128
        void ComputeNrTimeouts();
 
129
        ///
 
130
        void InitialiseBounds();
 
131
 
 
132
 
 
133
 
 
134
        /// Here come the reduction rules
 
135
 
 
136
 
 
137
 
 
138
        bool NodeReferredToBySomeInpredicate(Subject *n);
 
139
 
 
140
        bool VarTestedInHyperEdgeWithoutUpdate(ADSVar *v);
 
141
 
 
142
        bool VarUpdatedByTwoActivities(ADSVar *v);
 
143
 
 
144
        bool isRemovableHyperEdge(ADSHyperEdge *hedge, List <Node *> nodeused, List <ADSVar *> varused, bool reduction);
 
145
 
 
146
 private:
 
147
 
 
148
 
 
149
 
 
150
 
 
151
        /// the list of properties
 
152
        List <Prop *> propl;   
 
153
        ///     the list of variables
 
154
        List <ADSVar *> varl;  
 
155
        /// the variables updated in activities. Needed for deriving the interference relation
 
156
        List <ADSVar *> updatedinactivities; 
 
157
        /// the activities
 
158
        List <ADSActivity *> actlist;  
 
159
        /// n by n matrix (indexed by actlist)
 
160
        int interference[MAXACT][MAXACT];
 
161
        /// the list of properties that can be set by the environment
 
162
        List <Prop *> extproplist;
 
163
        /// the list of properties that are updated in activities 
 
164
        List <Prop *> intproplist; 
 
165
        /// the number of timeouts. Needed to initialise the interval of the clock manager
 
166
        int timeoutnumber;
 
167
        /// the bound of each node; needed for model checker input
 
168
        int bound[MAXNODE];
 
169
};
 
170
#endif