1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
/*
* PWList.hpp
*
* Created on: 01/03/2012
* Author: MathiasGS
*/
#ifndef WORKFLOWPWLIST_HPP_
#define WORKFLOWPWLIST_HPP_
#include "WaitingList.hpp"
#include <iostream>
#include "google/sparse_hash_map"
#include "NonStrictMarking.hpp"
#include "NonStrictMarking.hpp"
#include "WaitingList.hpp"
#include "PWList.hpp"
#include "CoveredMarkingVisitor.h"
namespace VerifyTAPN {
namespace DiscreteVerification {
class WorkflowPWListBasic : virtual public PWListBase
{
public:
virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep) = 0;
virtual NonStrictMarking* getUnpassed() = 0;
virtual bool add(NonStrictMarking* marking) = 0;
virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong) = 0;
virtual void addLastToWaiting() = 0;
virtual void setParent(NonStrictMarking*, NonStrictMarking*) = 0;
};
class WorkflowPWList : public WorkflowPWListBasic, public PWList {
private:
NonStrictMarking* last;
public:
WorkflowPWList(WaitingList<NonStrictMarking*>* w_l);
virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep);
virtual NonStrictMarking* getUnpassed();
virtual bool add(NonStrictMarking* marking);
virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong);
NonStrictMarking* lookup(NonStrictMarking* marking);
virtual void addLastToWaiting(){
waiting_list->add(last, last);
}
virtual void setParent(NonStrictMarking* marking, NonStrictMarking* parent)
{
marking->setParent(parent);
}
};
class WorkflowPWListHybrid : public WorkflowPWListBasic, public PWListHybrid {
private:
CoveredMarkingVisitor visitor;
ptriepointer_t<MetaData*> last_pointer;
public:
WorkflowPWListHybrid(TAPN::TimedArcPetriNet& tapn,
WaitingList<ptriepointer_t<MetaData*> >* w_l,
int knumber,
int nplaces,
int mage);
~WorkflowPWListHybrid();
virtual NonStrictMarking* getCoveredMarking(NonStrictMarking* marking, bool useLinearSweep);
virtual NonStrictMarking* getUnpassed();
virtual bool add(NonStrictMarking* marking);
virtual NonStrictMarking* addToPassed(NonStrictMarking* marking, bool strong);
virtual void addLastToWaiting();
virtual void setParent(NonStrictMarking* marking, NonStrictMarking*)
{
((MetaDataWithTraceAndEncoding*)marking->meta)->parent = parent;
}
};
} /* namespace DiscreteVerification */
} /* namespace VerifyTAPN */
#endif /* PWLIST_HPP_ */
|