-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprocesssystem.h
100 lines (80 loc) · 2.79 KB
/
processsystem.h
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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
#ifndef PROCESSSYSTEM_H
#define PROCESSSYSTEM_H
#include "filesystem.h"
#include "consoledock.h"
#include <QObject>
#include <QProcess>
class FileSystem;
class ProcessSystem : public QObject
{
Q_OBJECT
public:
ProcessSystem(FileSystem *fileSystem);
/**
* @brief setConsoleDock Assigns the console dock to the file system for logging
* @param consoleDock The console dock
*/
void setConsoleDock(ConsoleDock *consoleDock);
/**
* @brief verifyProperty Verifies a property using mcrl22lps, lps2pbes and pbes2bool
* @param property The property to verify
* @return The process id of the verification process
*/
int verifyProperty(Property *property);
/**
* @brief getResult Gets the result of a process
* for a verification process, the result is either "" (in case of error), "false" or "true"
* @param processid The id of the proces to get the result from
* @return The result of the process
*/
QString getResult(int processid);
signals:
void processFinished(int processid);
private:
FileSystem *fileSystem;
ConsoleDock *consoleDock;
int pid;
std::map<int, std::vector<QProcess*>> processes;
std::map<int, QString> results;
/**
* @brief mcrl22lps Executes mcrl22lps on the current specification
* @param verification Determines what console dock tab to use
*/
QProcess *createMcrl22lpsProcess(bool verification);
/**
* @brief lpsxsim Executes lpsxsim on the lps that corresponds to the current specification
*/
QProcess *createLpsxsimProcess();
/**
* @brief lps2lts Executes lps2lts on the lps that corresponds to the current specification
*/
QProcess *createLps2ltsProcess();
/**
* @brief ltsconvert Executes ltsconvert on the lts that corresponds to the current specification
*/
QProcess *createLtsconvertProcess();
/**
* @brief lps2pbes Executes lps2pbes on the lps that corresponds to the current specification and the given property
* @param propertyName The name of the property to include
*/
QProcess *createLps2pbesProcess(QString propertyName);
/**
* @brief pbes2bool Executes pbes2bool on the pbes that corresponds to the current specification and the given property
* @param propertyName The name of the property to include
*/
QProcess *createPbes2boolProcess(QString propertyName);
private slots:
/**
* @brief verifyProperty2 The second step of verification, creating the pbes
*/
void verifyProperty2();
/**
* @brief verifyPoperty3 The third step of verification, solving the pbes
*/
void verifyProperty3();
/**
* @brief actionVerifyResult Applies the result of the verification
*/
void verifyPropertyResult();
};
#endif // PROCESSSYSTEM_H