← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/sd/bv/adsvaluation.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/adsvaluation.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 _ADSVALUATION_H
 
22
#define _ADSVALUATION_H
 
23
 
 
24
#include "atdactionstatenode.h"
 
25
#include "lstring.h"
 
26
#include "subject.h"
 
27
#include "bag.h"
 
28
#include "node.h"
 
29
#include "adscks.h"
 
30
#include "llist.h"
 
31
#include "adsclockmanager.h"
 
32
 
 
33
class Clock;
 
34
class PropVal;
 
35
class OutputFile;
 
36
 
 
37
enum StateType {unstable, stable}; // in unstable state an event has occurred
 
38
 
 
39
/// Class to model the valuation of the state variables (configuration, terminated action state nodes, variables, clocks)
 
40
class ADSValuation: public Node {
 
41
/*@Doc: {\large {\bf scope:} } */
 
42
        public:
 
43
                /// 
 
44
                ADSValuation(ADSCks *c,StateType s );
 
45
                ///
 
46
                ~ADSValuation();
 
47
                ///
 
48
                Subject *Clone(){return new ADSValuation(*this);}
 
49
                ///
 
50
                ADSValuation(const ADSValuation &copy);
 
51
                ///
 
52
                ADSValuation(const ADSValuation &copy,StateType s);
 
53
                ///
 
54
                bool operator==( ADSValuation &comp);
 
55
                ///
 
56
                void Write(OutputFile *f) ;
 
57
                ///
 
58
                void  WriteScreen();
 
59
                ///
 
60
                void GetConfig(Bag <Subject *> *);
 
61
                ///
 
62
                void SetConfig(Bag <Subject *> c);
 
63
                ///
 
64
                void GetPropList(List <PropVal *> *);
 
65
                ///
 
66
                void SetPropList(List <PropVal *> p);
 
67
                ///
 
68
                                void GetQueue(List <PropVal *> *);
 
69
                ///
 
70
                        void SetQueue(List <PropVal *> p);
 
71
                ///
 
72
                void GetTerminated(Bag <ATDActionStateNode *> *);
 
73
                ///
 
74
                void AddTerminated(Bag <ATDActionStateNode *> t);
 
75
                ///
 
76
                     void GetQTerminated(Bag <ATDActionStateNode *> *);
 
77
                ///
 
78
                        void AddQTerminated(Bag <ATDActionStateNode *> t);
 
79
                ///
 
80
                ClockManager GetClockManager();
 
81
                ///
 
82
                void SetClockManager(ClockManager&);
 
83
                ///
 
84
                void GetClockConstraints(List <ClockConstraint *> *);
 
85
                ///
 
86
                void SetClockConstraints(List <ClockConstraint *> );
 
87
                ///
 
88
                void GetQClockConstraints(List <ClockConstraint *> *);
 
89
                ///
 
90
                void SetQClockConstraints(List <ClockConstraint *> );
 
91
                ///
 
92
                bool HasClockConstraints(){return (clist.count()>0);}
 
93
                /// set index for model checker input
 
94
                void SetNumber(int);
 
95
                /// get index for model checker input
 
96
                int GetNumber();
 
97
                ///
 
98
                bool isStable(){return (st==stable);}
 
99
                ///
 
100
                void makeStable(){st=stable;}
 
101
                /// get key
 
102
                int ComputeKey();
 
103
                ///
 
104
                bool hassameconfig( ADSValuation &comp);
 
105
 
 
106
 
 
107
        private:
 
108
                /// Configuration (containing nodes only)
 
109
                Bag <Subject *> cfg; //Nodes from hyperedge
 
110
                /// Terminated action state nodes
 
111
                Bag <ATDActionStateNode *> tlist; //Subbag from cfg
 
112
                /// Boolean properties valuations
 
113
                List <PropVal *> plist; // Abstraction from LVar + input
 
114
                /// Clock manager
 
115
                ClockManager cm;
 
116
                /// list of timeout events
 
117
                List <ClockConstraint *> clist; 
 
118
                ///
 
119
                StateType st; // stable or unstable
 
120
                ///
 
121
                int index; // index for for model checker input
 
122
                ///
 
123
                int key; // key for hashtable
 
124
                /*
 
125
                ///queue (only for implementation level semantics
 
126
                List <PropVal *> queue; 
 
127
                /// terminated activities (only for implementation level semantics)
 
128
                Bag <ATDActionStateNode *> qtermlist; //Subbag from terminated
 
129
                /// list of timeout events in ILS semantics
 
130
                List <ClockConstraint *> qclist; 
 
131
                */
 
132
};
 
133
 
 
134
#endif