LTL-Search/Model.h at cpp · ArmenSl/LTL-Search · GitHub

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
81
82
#pragma once
#include<vector>
#include<map>
#include<string>


enum class Interpretation
{
	UNKNOWN,
	TRUE,
	FALSE,
};

class InterpretationFunction
{
public:
	InterpretationFunction();
	InterpretationFunction(int stateCount);
	InterpretationFunction(InterpretationFunction&& interpretation) = default;
	InterpretationFunction(const InterpretationFunction& interpretation) = default;
	~InterpretationFunction();

	void setStateCount(int stateCount);

	///<summary> Get the value of a variable at a given state</summary>
	Interpretation get(int state, char name);

	void set(int state, char name, Interpretation i);
	const std::map<char, Interpretation>& getInterpretations(int state) const{ return this->interpretations[state]; }

	bool operator==(const InterpretationFunction& other) const;

	operator std::string() const;

private:
	std::vector<std::map<char, Interpretation>> interpretations;
};


class Transitions
{
public:
	Transitions();
	Transitions(int stateCount);
	~Transitions();

	void setStateCount(int stateCount);
	const std::vector<int>& getSuccessors(int state) const { return this->transitions[state]; };
	void setSuccessors(int state, const std::vector<int>& succs) { this->transitions[state] = succs; };
	void setSuccessors(int state, std::vector<int>&& succs) { this->transitions[state] = std::move(succs); };

	operator std::string() const;

private:
	std::vector<std::vector<int>> transitions;
};

class Model
{
public:

	Model(int stateCount);
	Model(const std::string & filepath, bool relative = true);
	~Model();
	const InterpretationFunction& getInterpretationFunction() const { return this->interpretationFunction; };
	const std::vector<int>& getSuccessors(int state) const { return this->transitions.getSuccessors(state); };

	//TODO just for test
	void setSuccessors(int state, const std::vector<int>& succs) { this->transitions.setSuccessors(state, succs); };
	void setInt(int state, char name, Interpretation inter) { this->interpretationFunction.set(state, name, inter); };
	int getStateCount() const { return this->stateCount; };

	operator std::string() const;


private:
	int stateCount;
	Transitions transitions;
	InterpretationFunction interpretationFunction;

};