Commit 23a50ad7 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Fixed imports. Added models as resources

parent 4b2a6468
......@@ -9,11 +9,13 @@ from learn.ra import RALearner
from sut import SUTType
from sut.fifoset import FIFOSetClass
from sut.login import new_login_sut, LoginClass
from test import IORATest, MealyTest
from test import IORATest
from test.rwalk import IORARWalkFromState, MealyRWalkFromState, DFARWalkFromState, RARWalkFromState
from tests.iora_testscenario import *
from encode.iora import IORAEncoder
# some example runs
def scrap_learn_iora():
learner = RALearner(IORAEncoder())
test_type = IORATest
......@@ -41,7 +43,7 @@ def scrap_learn_mbt_mealy():
print(model)
print(statistics)
def scrap_learn_mbt_mealy():
def scrap_learn_mbt_dfa():
learner = FALearner(DFAEncoder())
learner.set_timeout(100000)
login = LoginClass()
......@@ -61,6 +63,5 @@ def scrap_learn_mbt_ra():
print(model)
print(statistics)
#scrap_learn_mbt_mealy()
#scrap_learn_mbt_mealy()
scrap_learn_mbt_iora()
scrap_learn_mbt_mealy()
#scrap_learn_mbt_iora()
digraph g {
node [shape=oval];
11;
10;
26;
18;
31;
0 [peripheries=2,color="red"];
0 -> 10 [label="ITA/ONOK"];
0 -> 10 [label="IFAILEAC/ONOK"];
0 -> 10 [label="ICA/ONOK"];
0 -> 10 [label="IAA/ONOK"];
0 -> 10 [label="IREADFILE_0/ONOK"];
0 -> 10 [label="IFAILBAC/ONOK"];
0 -> 10 [label="ICOMPLETEBAC/ONOK"];
0 -> 11 [label="IGETCHALLENGE/OOK"];
0 -> 10 [label="IRESET/OOK"];
10 -> 10 [label="ITA/ONOK"];
10 -> 10 [label="IFAILEAC/ONOK"];
10 -> 10 [label="ICA/ONOK"];
10 -> 10 [label="IAA/ONOK"];
10 -> 10 [label="IREADFILE_0/ONOK"];
10 -> 10 [label="IFAILBAC/ONOK"];
10 -> 10 [label="ICOMPLETEBAC/ONOK"];
10 -> 11 [label="IGETCHALLENGE/OOK"];
10 -> 10 [label="IRESET/OOK"];
11 -> 10 [label="IFAILBAC/ONOK"];
11 -> 10 [label="IRESET/OOK"];
11 -> 11 [label="IGETCHALLENGE/OOK"];
11 -> 11 [label="IFAILEAC/ONOK"];
11 -> 11 [label="ITA/ONOK"];
11 -> 11 [label="ICA/ONOK"];
11 -> 11 [label="IREADFILE_0/ONOK"];
11 -> 11 [label="IAA/ONOK"];
11 -> 18 [label="ICOMPLETEBAC/OOK"];
18 -> 10 [label="IFAILBAC/ONOK"];
18 -> 10 [label="IRESET/OOK"];
18 -> 18 [label="IREADFILE_0/ONOK"];
18 -> 26 [label="IFAILEAC/ONOK"];
18 -> 26 [label="ICA/OOK"];
18 -> 18 [label="ITA/ONOK"];
18 -> 18 [label="IAA/OOK"];
18 -> 10 [label="ICOMPLETEBAC/ONOK"];
18 -> 10 [label="IGETCHALLENGE/ONOK"];
26 -> 10 [label="IFAILBAC/ONOK"];
26 -> 10 [label="IRESET/OOK"];
26 -> 26 [label="IFAILEAC/ONOK"];
26 -> 26 [label="IREADFILE_0/ONOK"];
26 -> 31 [label="ITA/OOK"];
26 -> 26 [label="ICA/OOK"];
26 -> 26 [label="IAA/OOK"];
26 -> 10 [label="ICOMPLETEBAC/ONOK"];
26 -> 10 [label="IGETCHALLENGE/ONOK"];
31 -> 31 [label="IREADFILE_0/ONOK"];
31 -> 31 [label="ITA/OOK"];
31 -> 31 [label="ICA/OOK"];
31 -> 31 [label="IAA/OOK"];
31 -> 26 [label="IFAILEAC/ONOK"];
31 -> 10 [label="ICOMPLETEBAC/ONOK"];
31 -> 10 [label="IGETCHALLENGE/ONOK"];
31 -> 10 [label="IFAILBAC/ONOK"];
31 -> 10 [label="IRESET/OOK"];
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s3 [shape="circle" label="3"];
s4 [shape="circle" label="4"];
s5 [shape="circle" label="5"];
s6 [shape="circle" label="6"];
s7 [shape="circle" label="7"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s1 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s3 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s4 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s5 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s5 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s6 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s6 -> s6 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s7 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s7 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
__start0 -> s0;
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s1 -> s2 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s2 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
__start0 -> s0;
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s3 [shape="circle" label="3"];
s4 [shape="circle" label="4"];
s5 [shape="circle" label="5"];
s6 [shape="circle" label="6"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s1 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s3 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s4 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s5 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s5 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s6 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s6 -> s6 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
__start0 -> s0;
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s3 [shape="circle" label="3"];
s4 [shape="circle" label="4"];
s5 [shape="circle" label="5"];
s6 [shape="circle" label="6"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s1 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s3 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s4 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s5 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s5 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s5 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s6 -> s3 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s6 -> s6 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s6 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
__start0 -> s0;
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s3 [shape="circle" label="3"];
s4 [shape="circle" label="4"];
s5 [shape="circle" label="5"];
s6 [shape="circle" label="6"];
s7 [shape="circle" label="7"];
s8 [shape="circle" label="8"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s1 [label="|Pds(StateVideoOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s1 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s5 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s3 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s3 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s6 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s7 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s4 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s5 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s6 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s7 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s7 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s7 -> s8 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s8 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s8 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s8 -> s8 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s8 -> s8 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
__start0 -> s0;
}
digraph g {
__start0 [label="" shape="none"];
s0 [shape="circle" label="0"];
s1 [shape="circle" label="1"];
s2 [shape="circle" label="2"];
s3 [shape="circle" label="3"];
s4 [shape="circle" label="4"];
s5 [shape="circle" label="5"];
s6 [shape="circle" label="6"];
s7 [shape="circle" label="7"];
s8 [shape="circle" label="8"];
s0 -> s1 [label="|Pds(StateSystemOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s1 [label="|Pds(StateVideoOn)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s0 -> s2 [label="|Pds(StateSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s1 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s1 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s1 -> s1 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s1 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s5 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s3 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s3 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s3 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s3 -> s1 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running)|"];
s3 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Pds(ButtonSystemOff)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s6 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s4 -> s4 [label="|Host(openProfileStartApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s4 [label="|Host(openProfileStopApplication)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s4 -> s7 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s4 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(Shutdown)|"];
s5 -> s3 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s5 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s5 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Stopped)|"];
s5 -> s3 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s6 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s6 -> s6 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s6 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s6 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s7 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s7 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s7 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s7 -> s8 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s7 [label="|OS(StartPcs)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s7 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s2 [label="|Pds(ButtonSystemOff)| / |PCS(Running);SM1(Stopped);SM2(Stopped);Dev(OpenProfile);Dev(Shutdown)|"];
s8 -> s4 [label="|Host(stopForInstallation)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s8 [label="|Host(startAfterInstallation)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s4 [label="|Host(goToOpenProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
s8 -> s3 [label="|Host(goToClosedProfile)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped)|"];
s8 -> s8 [label="|Host(openProfileStartApplication)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s7 [label="|Host(openProfileStopApplication)| / |PCS(Running);SM1(Stopped);SM2(Running);Dev(OpenProfile)|"];
s8 -> s8 [label="|OS(StartPcs)| / |PCS(Running);SM1(Running);SM2(Running);Dev(OpenProfile)|"];
s8 -> s4 [label="|OS(StopPcs)| / |PCS(Stopped);SM1(Stopped);SM2(Stopped);Dev(OpenProfile)|"];
__start0 -> s0;
}
from abc import ABCMeta, abstractmethod
import z3
def enum(name, elements):
d = z3.Datatype(name)
for element in elements:
......
import collections
from abc import ABCMeta, abstractmethod
import z3
from define import enum, Automaton
import model.fa
from define import enum, Automaton
from model import Transition
......
from collections import namedtuple
import z3
from model.ra import *
from define import enum
from define import Automaton
from define import enum, Automaton
class RegisterMachine(Automaton):
......
from abc import ABCMeta, abstractmethod
import z3
from define import Automaton
......
import itertools
import z3
from define.fa import DFA, MealyMachine, Mapper
from encode import Encoder
from utils import Tree
#from model.fa import MealyMachine
import z3
class DFAEncoder(Encoder):
......
import itertools
import z3
from define.ra import IORegisterAutomaton, Mapper
from encode import Encoder
from sut import ActionSignature
from utils import Tree, determinize
......
import itertools
import z3
import z3
from encode import Encoder
from define.ra import IORegisterAutomaton2, Mapper
from utils import Tree, determinize
......
import itertools
import z3
import z3
from encode import Encoder
from define.ra import RegisterAutomaton, Mapper
from utils import Tree, determinize
......
from typing import List, Tuple, Union
from typing import cast
import collections
from typing import List, Tuple, Union,cast
from model import Automaton
from learn import Learner
......
from typing import Tuple
import z3
from encode.ra import RAEncoder
from learn import Learner
import model.fa
import z3
from encode.fa import DFAEncoder, MealyEncoder
from learn import Learner
from model import Automaton
import define.fa
......@@ -45,19 +37,15 @@ class FALearner(Learner):
"""generates the definition and model for an fa whose traces include the traces added so far
In case of failure, the second argument of the tuple signals occurrence of a timeout"""
for num_states in range(min_states, max_states + 1):
print("Learning with ", num_states, " states")
fa, constraints = self.encoder.build(num_states)
self.solver.reset()
self.solver.add(constraints)
if self.timeout is not None:
self.solver.set("timeout", self.timeout)
print(self.solver.to_smt2())
result = self.solver.check()
print(self.solver.statistics())
if self.verbose:
print("Learning with {0} states. Result: {1}"
.format(num_states, result))
print("Result {0} ".format(result))
if result == z3.sat:
model = self.solver.model()
return (True, fa, model)
......