-
Notifications
You must be signed in to change notification settings - Fork 5
/
buildFaultyExecutionsGraph.py
95 lines (76 loc) · 5.54 KB
/
buildFaultyExecutionsGraph.py
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
from useCases.DependencyGraph import DependencyGraph
from useCases.DependencyGraph2 import DependencyGraph2
from useCases.StateOfNodesDependencyGraph import StateOfNodesDependencyGraph
from useCases.AlternativeReceives import AlternativeReceives
from useCases.ReceivesDependencyGraph import ReceivesDependencyGraph
from useCases.ModifiedReceivesDependencyGraph import ModifiedReceivesDependencyGraph
import argparse
import pdb
from utils.Traces import ExperimentTraces, Trace
import z3
"""
this file creates traces from the logs of leader-election executions. The logs are created by hand from the automatic ones (folder "evenMoreAlternative") [the question is
what is the right representation. if the logs are passed "as-is", the returned formula is something like
"F(proc1 declares himself as a leader AND proc2 declares himself as a follower)"
The result of running this script is a traces file (defined by --traces_out option) that can be used to obtain LTL formula from it.
The way to run:
python buildFaultyExecutionsGraph.py --property_file_faulty useCases/PCTCP/evenMoreAlternative/faultyExample.execution --property_file_correct useCases/PCTCP/evenMoreAlternative/correctMirror.execution useCases/PCTCP/evenMoreAlternative/0ReceivedFrom1.execution useCases/PCTCP/evenMoreAlternative/0CommitsYetCorrect.execution useCases/PCTCP/evenMoreAlternative/correctAfterAll.execution --traces_out=traces/useCases/statePtcp/state.trace
"""
if __name__ == "__main__":
parser = argparse.ArgumentParser()
parser.add_argument("--property_file_faulty", dest="propertyFileFaulty", nargs='+', default=[\
"useCases/newPCTCPData/experiments/pctcp-d2-nocrash-modified/135/execution",\
])
parser.add_argument("--property_file_correct", dest="propertyFileCorrect", nargs='+', default=[\
#"useCases/newPCTCPData/experiments/pctcp-d2-nocrash/136/execution",\
#"useCases/newPCTCPData/experiments/pctcp-d2-nocrash/816/execution",\
# "useCases/newPCTCPData/experiments/pctcp-d2-nocrash/456/execution",\
# "useCases/newPCTCPData/experiments/pctcp-d2-nocrash/208/execution",\
# "useCases/newPCTCPData/experiments/pctcp-d2-nocrash/1/execution",\
"useCases/newPCTCPData/experiments/pctcp-d2-nocrash-modified/2/execution",\
#"useCases/newPCTCPData/experiments/pctcp-d2-nocrash/3/execution",\
#"useCases/newPCTCPData/experiments/pctcp-d2-nocrash/4/execution",\
])
parser.add_argument("--traces_out", dest="tracesFileName", default="traces/useCases/ptcp-d2-nocrash/generated.trace")
parser.add_argument("--num_linearization", dest="numTracesLinearizations", type=int, default=5)
args,unknown = parser.parse_known_args()
faultyTraces = None
correctTraces = None
faultyExecutions = args.propertyFileFaulty
correctExecutions = args.propertyFileCorrect
#depGraph = StateOfNodesDependencyGraph
#depGraph = DependencyGraph
#depGraph = ReceivesDependencyGraph
#depGraph = AlternativeReceives
depGraph = DependencyGraph2
depGraph = ModifiedReceivesDependencyGraph
for fileName in faultyExecutions:
print(fileName)
dgF = depGraph()
dgF.readGraphFromPropertyFile(fileName)
newTraces = dgF.generateTraces(maxNumberOfSolutions = args.numTracesLinearizations)
if faultyTraces == None:
faultyTraces = newTraces
else:
faultyTraces += newTraces
for fileName in correctExecutions:
dgF = depGraph()
dgF.readGraphFromPropertyFile(fileName)
newTraces = dgF.generateTraces(maxNumberOfSolutions = args.numTracesLinearizations)
if correctTraces == None:
correctTraces = newTraces
else:
correctTraces += newTraces
experimentTraces = ExperimentTraces(tracesToAccept = [Trace(traceVector = faultyTr, lassoStart = (len(faultyTr)-1)) for faultyTr in faultyTraces],\
tracesToReject = [Trace(traceVector = correctTr, lassoStart = (len(correctTr)-1)) for correctTr in correctTraces], depth = 10)
for trace in correctTraces:
if trace in faultyTraces:
print("problem!")
print(trace)
pdb.set_trace()
for trace in faultyTraces:
if trace in correctTraces:
print("problem2!")
pdb.set_trace()
fileToWrite = args.tracesFileName
experimentTraces.writeTracesToFile(fileToWrite)