Skip to content

GitLab

mohawk-2.0
mohawk-2.0
Commit 8df1fdc7 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files
Options

Extended and changed the option NOREFINE to SKIPREFINE and implemented it in... 

Extended and changed the option NOREFINE to SKIPREFINE and implemented it in the RUN ALL section; fixed recording of results; Increased version v2.2.0
parent c0e3780b
Hide whitespace changes
Inline Side-by-side
Showing with 281 additions and 67 deletions
logs/2015-09-17 results/ASASPTime_Results.csv 0 → 100644
View file @ 8df1fdc7
File,Raw Result,Result,Duration (s),Comment
Testcases/Separate_Assumption/c1,System is UNSAFE,GOAL_REACHABLE,1.11,
Testcases/Separate_Assumption/c2,System is SAFE,GOAL_UNREACHABLE,0.02,
Testcases/Separate_Assumption/c3,System is UNSAFE,GOAL_REACHABLE,0.79,
Testcases/Separate_Assumption/c4,System is UNSAFE,GOAL_REACHABLE,1.24,
Testcases/Separate_Assumption/c5,System is UNSAFE,GOAL_REACHABLE,2.20,
Testcases/Separate_Assumption/c6,System is UNSAFE,GOAL_REACHABLE,2.75,
Testcases/Separate_Assumption/c7,System is SAFE,GOAL_UNREACHABLE,0.02,
Testcases/Separate_Assumption/c8,System is UNSAFE,GOAL_REACHABLE,0.98,
Testcases/Separate_Assumption/c9,System is UNSAFE,GOAL_REACHABLE,1.11,
Testcases/Separate_Assumption/c10,System is UNSAFE,GOAL_REACHABLE,1.20,
Testcases/Separate_Assumption/c11,System is UNSAFE,GOAL_REACHABLE,1.62,
Testcases/Separate_Assumption/c12,System is UNSAFE,GOAL_REACHABLE,1.60,
Testcases/Separate_Assumption/c13,System is UNSAFE,GOAL_REACHABLE,2.93,
Testcases/NonSeparate_Assumption/AGTUniv1,System is SAFE,GOAL_UNREACHABLE,0.21,
Testcases/NonSeparate_Assumption/AGTUniv2,System is UNSAFE,GOAL_REACHABLE,0.41,
Testcases/NonSeparate_Assumption/AGTUniv3,System is SAFE,GOAL_UNREACHABLE,0.28,
Testcases/NonSeparate_Assumption/AGTUniv4,System is SAFE,GOAL_UNREACHABLE,1.18,
Testcases/NonSeparate_Assumption/AGTUniv5,System is UNSAFE,GOAL_REACHABLE,7.87,
Testcases/NonSeparate_Assumption/AGTUniv6,System is UNSAFE,GOAL_REACHABLE,2.09,
Testcases/NonSeparate_Assumption/AGTUniv7,System is SAFE,GOAL_UNREACHABLE,0.38,
Testcases/NonSeparate_Assumption/AGTUniv8,System is UNSAFE,GOAL_REACHABLE,0.92,
Testcases/NonSeparate_Assumption/AGTUniv9,System is UNSAFE,GOAL_REACHABLE,3.27,
Testcases/NonSeparate_Assumption/AGTUniv10,System is UNSAFE,GOAL_REACHABLE,5.76,
Testcases/NonSeparate_Assumption/AGTHos1,System is SAFE,GOAL_UNREACHABLE,0.29,
Testcases/NonSeparate_Assumption/AGTHos2,System is UNSAFE,GOAL_REACHABLE,0.38,
Testcases/NonSeparate_Assumption/AGTHos3,System is UNSAFE,GOAL_REACHABLE,0.53,
Testcases/NonSeparate_Assumption/AGTHos4,System is SAFE,GOAL_UNREACHABLE,0.22,
Testcases/NonSeparate_Assumption/AGTHos5,System is UNSAFE,GOAL_REACHABLE,0.76,
Testcases/NonSeparate_Assumption/AGTHos6,System is UNSAFE,GOAL_REACHABLE,1.18,
Testcases/NonSeparate_Assumption/AGTHos7,System is SAFE,GOAL_UNREACHABLE,0.29,
Testcases/NonSeparate_Assumption/AGTHos8,System is UNSAFE,GOAL_REACHABLE,1.62,
Testcases/NonSeparate_Assumption/AGTHos9,System is UNSAFE,GOAL_REACHABLE,0.73,
Testcases/NonSeparate_Assumption/AGTHos10,System is UNSAFE,GOAL_REACHABLE,0.85,
logs/2015-09-17 results/Commands.txt 0 → 100644
View file @ 8df1fdc7
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c1
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c2
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c3
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c4
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c5
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c6
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c7
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c8
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c9
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c10
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c11
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c12
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rSA Testcases/Separate_Assumption/c13
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv1
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv2
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv3
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv4
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv5
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv6
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv7
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv8
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv9
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTUniv10
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos1
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos2
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos3
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos4
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos5
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos6
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos7
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos8
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos9
/usr/bin/time -f "Duration: %e sec" ./ASASystem.py -rNSA Testcases/NonSeparate_Assumption/AGTHos10
logs/2015-09-17 results/MohawkResults.csv 0 → 100644
View file @ 8df1fdc7
File,Result,Duration (ms),Comment,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test01.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,2,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test01.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,80,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test01.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,79,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test02.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,32,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test03.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,130,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test04.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,34,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test05.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,47,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test06.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,195,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test07.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,1410,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test08.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,27639,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test09.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,72717,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\positive\test10.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,121222,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test01.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,119,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test02.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,76,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test03.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,85,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test04.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,97,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test05.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,43,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test06.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,87,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test07.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,982,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test08.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,22145,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test09.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,59045,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixednocr\test10.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,96491,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test01.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,120,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test02.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,78,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test03.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,86,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test04.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,105,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test05.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,41,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test06.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,90,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test07.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,981,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test08.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,22674,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test09.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,59940,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\Mohawk\mixed\test10.mohawk.mohawk.T.mohawk,GOAL_REACHABLE,97973,Mode: BMC; SkipRefine: false,,,,File,Raw Result,Result,Same Result?,Duration (s),Comment
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c01.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,148,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c1,System is UNSAFE,GOAL_REACHABLE,TRUE,1.11,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c02.asaptime.sa.mohawk.T.mohawk,GOAL_UNREACHABLE,62,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c2,System is SAFE,GOAL_UNREACHABLE,TRUE,0.02,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c03.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,72,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c3,System is UNSAFE,GOAL_REACHABLE,TRUE,0.79,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c04.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,72,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c4,System is UNSAFE,GOAL_REACHABLE,TRUE,1.24,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c05.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,126,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c5,System is UNSAFE,GOAL_REACHABLE,TRUE,2.2,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c06.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,79,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c6,System is UNSAFE,GOAL_REACHABLE,TRUE,2.75,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c07.asaptime.sa.mohawk.T.mohawk,GOAL_UNREACHABLE,51,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c7,System is SAFE,GOAL_UNREACHABLE,TRUE,0.02,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c08.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,55,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c8,System is UNSAFE,GOAL_REACHABLE,TRUE,0.98,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c09.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,57,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c9,System is UNSAFE,GOAL_REACHABLE,TRUE,1.11,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c10.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,67,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c10,System is UNSAFE,GOAL_REACHABLE,TRUE,1.2,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c11.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,64,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c11,System is UNSAFE,GOAL_REACHABLE,TRUE,1.62,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c12.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,57,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c12,System is UNSAFE,GOAL_REACHABLE,TRUE,1.6,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuiteb\c13.asaptime.sa.mohawk.T.mohawk,GOAL_REACHABLE,72,Mode: BMC; SkipRefine: false,,,,Testcases/Separate_Assumption/c13,System is UNSAFE,GOAL_REACHABLE,TRUE,2.93,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos01.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,8284,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos1,System is SAFE,GOAL_UNREACHABLE,TRUE,0.29,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos01.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,12445,Mode: BMC; SkipRefine: true,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,18487,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos2,System is UNSAFE,GOAL_REACHABLE,TRUE,0.38,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,534,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,579,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,531,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,18593,Mode: BMC; SkipRefine: true,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos03.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,475,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos3,System is UNSAFE,GOAL_REACHABLE,TRUE,0.53,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos03.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,549,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos04.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,10011,Mode: BMC; SkipRefine: true,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos04.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,NaN,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos4,System is SAFE,GOAL_UNREACHABLE,TRUE,0.22,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos05.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,14285,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos5,System is UNSAFE,GOAL_REACHABLE,FALSE,0.76,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos06.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,3028,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos6,System is UNSAFE,GOAL_REACHABLE,TRUE,1.18,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos07.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,31311,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos7,System is SAFE,GOAL_UNREACHABLE,TRUE,0.29,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos07.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,29281,Mode: BMC; SkipRefine: true,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos08.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,962027,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos8,System is UNSAFE,GOAL_REACHABLE,FALSE,1.62,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos09.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,77747,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos9,System is UNSAFE,GOAL_REACHABLE,FALSE,0.73,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\hos\AGTHos10.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,NaN,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTHos10,System is UNSAFE,GOAL_REACHABLE,FALSE,0.85,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv01.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,6733,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv1,System is SAFE,GOAL_UNREACHABLE,TRUE,0.21,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,3110,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv2,System is UNSAFE,GOAL_REACHABLE,TRUE,0.41,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv03.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,16952,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv3,System is SAFE,GOAL_UNREACHABLE,TRUE,0.28,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv04.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,7885,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv4,System is SAFE,GOAL_UNREACHABLE,FALSE,1.18,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv05.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,4701,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv5,System is UNSAFE,GOAL_REACHABLE,TRUE,7.87,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv06.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,46341,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv6,System is UNSAFE,GOAL_REACHABLE,FALSE,2.09,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv01.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,77497,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv02.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,213,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv03.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,361221,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv04.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,1188,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv05.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,2494,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\AGTUniv06.asaptime.nsa.mohawk.T.mohawk,GOAL_REACHABLE,16232,Mode: BMC; SkipRefine: false,,,,,,,,,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\large\AGTUniv07.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,24841,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv7,System is SAFE,GOAL_UNREACHABLE,TRUE,0.38,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\large\AGTUniv08.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,180899,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv8,System is UNSAFE,GOAL_REACHABLE,FALSE,0.92,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\large\AGTUniv09.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,274287,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv9,System is UNSAFE,GOAL_REACHABLE,FALSE,3.27,
D:\Work\Masters\workspace\Mohawk 2.0\data\ranise\testsuitec\univ\large\AGTUniv10.asaptime.nsa.mohawk.T.mohawk,GOAL_UNREACHABLE,58446,Mode: BMC; SkipRefine: true,,,,Testcases/NonSeparate_Assumption/AGTUniv10,System is UNSAFE,GOAL_REACHABLE,FALSE,5.76,
src/mohawk/MohawkInstance.java
View file @ 8df1fdc7
......@@ -13,13 +13,6 @@ import java.util.logging.Handler;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.global.formatter.MohawkCSVFileFormatter;
import mohawk.global.formatter.MohawkConsoleFormatter;
import mohawk.global.results.MohawkResults;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.testing.TestingSuite;
import org.apache.commons.cli.BasicParser;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.CommandLineParser;
......@@ -29,6 +22,13 @@ import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import org.apache.commons.lang3.StringUtils;
import mohawk.global.formatter.MohawkCSVFileFormatter;
import mohawk.global.formatter.MohawkConsoleFormatter;
import mohawk.global.results.MohawkResults;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.testing.TestingSuite;
/**
*
* @author Jonathan Shahen
......@@ -36,7 +36,7 @@ import org.apache.commons.lang3.StringUtils;
*/
public class MohawkInstance {
private final String VERSION = "v2.1.2";
private final String VERSION = "v2.2.0";
private static final String AUTHORS = "Jonathan Shahen <jmshahen [AT] uwaterloo [DOT] ca>; Karthick Jayaraman";
// Logger Fields
......@@ -47,7 +47,7 @@ public class MohawkInstance {
private Level LoggerLevel;
private FileHandler fileHandler;
private Boolean WriteCSVFileHeader = true;
private String resultsFile = "latestMohawkResults.csv";
private String resultsFile = "logs/MohawkResults.csv";
private String timingFile = "logs/MohawkTiming.csv";
// Reference
......@@ -84,6 +84,8 @@ public class MohawkInstance {
results = new MohawkResults();
timing = new MohawkTiming();
tests = new TestingSuite(SMV_helper, results, timing);
tests.testingResultsFile = resultsFile;
tests.skipRefine = SMV_helper.skipRefine;
if (cmd.hasOption(OptionString.NOSLICING.toString())) {
logger.fine("[OPTION] RBAC Slicing is OFF");
......@@ -140,7 +142,7 @@ public class MohawkInstance {
logger.info("[EOF] Mohawk is done running");
for (Handler h : logger.getHandlers()) {
h.close(); //must call h.close or a .LCK file will remain.
h.close();//must call h.close or a .LCK file will remain.
}
return 0;
......@@ -171,7 +173,8 @@ public class MohawkInstance {
.withArgName("quiet|debug|verbose")
.withDescription(
"Be extra quiet only errors are shown; " + "Show debugging information; "
+ "extra information is given for Verbose; " + "default is warning level").hasArg()
+ "extra information is given for Verbose; " + "default is warning level")
.hasArg()
.create(OptionString.LOGLEVEL.toString()));
options.addOption(OptionBuilder
......@@ -180,14 +183,16 @@ public class MohawkInstance {
"The filepath where the log file should be created; "
+ "No file will be created when equal to 'n'; "
+ "A unique filename will be created when equal to 'u'; "
+ "default it creates a log called '" + Logger_filepath + "'").hasArg()
+ "default it creates a log called '" + Logger_filepath + "'")
.hasArg()
.create(OptionString.LOGFILE.toString()));
options.addOption(OptionBuilder
.withArgName("folderpath")
.withDescription(
"The folderpath where the log file should be created; "
+ "default it creates in the current directory").hasArg()
+ "default it creates in the current directory")
.hasArg()
.create(OptionString.LOGFOLDER.toString()));
options.addOption(OptionString.NOHEADER.toString(), false,
......@@ -219,14 +224,16 @@ public class MohawkInstance {
.withDescription(
"The file/folder path where the SMV file(s) should be created; "
+ "Only temporary files will be used when equal to 'n'; "
+ "by default it creates a SMV called '" + SMV_helper.smvFilepath + "'").hasArg()
+ "by default it creates a SMV called '" + SMV_helper.smvFilepath + "'")
.hasArg()
.create(OptionString.SMVFILE.toString()));
options.addOption(OptionBuilder
.withArgName("extension")
.withDescription(
"File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
+ SMV_helper.specFileExt + "'").hasArg().create(OptionString.SPECEXT.toString()));
+ SMV_helper.specFileExt + "'")
.hasArg().create(OptionString.SPECEXT.toString()));
// Add Functional Options
options.addOption(OptionString.BULK.toString(), false,
......@@ -235,21 +242,23 @@ public class MohawkInstance {
"Turns off the slicing of the RBAC Input Spec file (Slices by default)");
options.addOption(OptionString.SLICEQUERY.toString(), false,
"Turns on the slicing of the RBAC Input Spec Query (Does not slice by default)");
options.addOption(OptionString.NOREFINE.toString(), false,
options.addOption(OptionString.SKIPREFINE.toString(), false,
"Turns off the refining step of the RBAC Input Spec (Refines by default)");
options.addOption(OptionBuilder
.withArgName("bmc|smc|both")
.withDescription(
"Uses the Bound Estimation Checker when equal to 'bmc'; "
+ "Uses Symbolic Model Checking when equal to 'smc'").hasArg()
+ "Uses Symbolic Model Checking when equal to 'smc'")
.hasArg()
.create(OptionString.MODE.toString()));
options.addOption(OptionBuilder
.withArgName("seconds")
.withDescription(
"The timeout time in seconds for Mohawk's refinement loop. Default: "
+ SMV_helper.TIMEOUT_SECONDS).hasArg().create(OptionString.TIMEOUT.toString()));
+ SMV_helper.TIMEOUT_SECONDS)
.hasArg().create(OptionString.TIMEOUT.toString()));
// Add Actionable Options
options.addOption(OptionBuilder
......@@ -257,7 +266,8 @@ public class MohawkInstance {
.withDescription(
"Runs the whole model checker when equal to 'all'; "
+ "Runs only the SMV conversion when equal to 'smv'; "
+ "Calculates the diameter when equal to 'dia'").hasArg()
+ "Calculates the diameter when equal to 'dia'")
.hasArg()
.create(OptionString.RUN.toString()));
}
......@@ -301,11 +311,12 @@ public class MohawkInstance {
}
// Turn off refining of the RBAC File
if (cmd.hasOption(OptionString.NOREFINE.toString())) {
if (cmd.hasOption(OptionString.SKIPREFINE.toString())) {
logger.fine("[OPTION] RBAC Role Refining is OFF");
SMV_helper.refineRoles = false;
SMV_helper.skipRefine = true;
} else {
logger.fine("[OPTION] RBAC Role Refining is ON");
SMV_helper.skipRefine = false;
}
// Grab the SPEC file
......@@ -388,7 +399,7 @@ public class MohawkInstance {
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.FINEST); // Default Level
setLoggerLevel(Level.FINEST);// Default Level
if (cmd.hasOption(OptionString.LOGLEVEL.toString())) {
String loglevel = cmd.getOptionValue(OptionString.LOGLEVEL.toString());
if (loglevel.equalsIgnoreCase("quiet")) {
......@@ -445,7 +456,7 @@ public class MohawkInstance {
Logger_filepath = logfile.getAbsolutePath();
if (WriteCSVFileHeader) {
FileOutputStream writer = new FileOutputStream(logfile, true); // Always append!
FileOutputStream writer = new FileOutputStream(logfile, true);// Always append!
writer.write(MohawkCSVFileFormatter.csvHeaders().getBytes());
writer.flush();
writer.close();
......@@ -490,7 +501,7 @@ public class MohawkInstance {
logger.fine("[OPTION] Checking the NuSMV version number");
String[] commands = { NuSMV_filepath, "-help" };
ProcessBuilder pb = new ProcessBuilder(commands);
pb.redirectErrorStream(true); // REQUIRED: NuSVM uses STDERR
pb.redirectErrorStream(true);// REQUIRED: NuSVM uses STDERR
// will throw error if it cannot find NuSMV
Process proc = pb.start();
......
src/mohawk/OptionString.java
View file @ 8df1fdc7
......@@ -2,9 +2,12 @@ package mohawk;
public enum OptionString {
HELP("help"), AUTHORS("authors"), VERSION("version"), CHECKNUSMV("checknusmv"), LOGLEVEL("loglevel"), LOGFILE(
"logfile"), LOGFOLDER("logfolder"), NOHEADER("noheader"), RESULTSFILE("output"), MAXW("maxw"), LINESTR(
"linstr"), SPECFILE("input"), SMVFILE("smvfile"), SPECEXT("specext"), BULK("bulk"), NOSLICING("noslicing"), SLICEQUERY(
"slicequery"), MODE("mode"), TIMEOUT("timeout"), RUN("run"), NUSMVPATH("nusmv"), NOREFINE("norefine");
"logfile"),
LOGFOLDER("logfolder"), NOHEADER("noheader"), RESULTSFILE("output"), MAXW("maxw"), LINESTR(
"linstr"),
SPECFILE("input"), SMVFILE("smvfile"), SPECEXT("specext"), BULK("bulk"), NOSLICING("noslicing"), SLICEQUERY(
"slicequery"),
MODE("mode"), TIMEOUT("timeout"), RUN("run"), NUSMVPATH("nusmv"), SKIPREFINE("skiprefine");
private String _str;
......
src/mohawk/helper/SMVSpecHelper.java
View file @ 8df1fdc7
......@@ -22,13 +22,13 @@ public class SMVSpecHelper {
public String specFile = "";
public String specFileExt = ".mohawk";
public ArrayList<File> specFiles = new ArrayList<File>();
public int mode = 3; // 1 for bmc, 2 for smc, 3 for both
public Long TIMEOUT_SECONDS = (long) 0; // Default infinite
public int mode = 3;// 1 for bmc, 2 for smc, 3 for both
public Long TIMEOUT_SECONDS = (long) 0;// Default infinite
public boolean bulk = false;
public Boolean smvDeleteFile = false;
public boolean sliceRBAC = true;
public boolean sliceRBACQuery = false;
public boolean refineRoles = true;
public boolean skipRefine = true;
public void loadSpecFiles() throws IOException {
if (this.bulk == true) {
......@@ -117,13 +117,13 @@ public class SMVSpecHelper {
rbac = scRole.getSlicedPolicy();
}
if (refineRoles) {
if (skipRefine) {
nusmv.fillAttributes(rbac);
} else {
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
RBACInstance rbac_refined = absrefine.refineOnly();
nusmv.fillAttributes(rbac_refined);
} else {
nusmv.fillAttributes(rbac);
}
nusmv.writeFile();
} catch (IOException e1) {
......
src/mohawk/refine/RolesAbsRefine.java
View file @ 8df1fdc7
......@@ -34,7 +34,7 @@ public class RolesAbsRefine {
public RolesAbsRefine(RBACInstance inRbac) {
mode = NuSMVMode.BMC; // Default mode is BMC
mode = NuSMVMode.BMC;// Default mode is BMC
k = 2;
lastpriority = 0;
unsliced = inRbac;
......@@ -158,8 +158,8 @@ public class RolesAbsRefine {
return false;
// Set<String> incrementRoles = rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>(); // =
// rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>();// =
// rdeptree.getRoles(refinementstep);
for (int i = 0; i < k; i++) {
Set<String> sNextQueue = this.rdeptree.getRoles(lastpriority);
if (sNextQueue != null) {
......@@ -242,7 +242,7 @@ public class RolesAbsRefine {
if (UnSlicedCond.size() > 0) {
for (int i : UnSlicedCond.keySet()) {
if (mMapping.containsKey(i)) {
int iNewIndex = mMapping.get(i); // getNewRoleIndex(i);
int iNewIndex = mMapping.get(i);// getNewRoleIndex(i);
SlicedCond.addConditional(iNewIndex, UnSlicedCond.getConditional(i));
}
}
......@@ -302,14 +302,30 @@ public class RolesAbsRefine {
return result;
}
public Boolean getResult(RBACInstance curInstance, Integer fileno) throws IOException, InterruptedException {
WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, "smvtemplate");
nusmv.fillAttributes(curInstance);
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC) {
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(curInstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
curInstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
} else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
return result;
}
public ExecutionResult absrefineloop() {
int fileno = 1;
Integer fileno = 1;
try {
while (refine()) {
WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, "smvtemplate");
nusmv.fillAttributes(nextinstance);
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
try {
writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
......@@ -320,18 +336,7 @@ public class RolesAbsRefine {
System.out.printf("\n\n-----\n Starting Refinement Step %d, with %d Roles and %d Rules\n", fileno,
nextinstance.getNumRoles(), nextinstance.getNumRules());
// NuSMV bmc
Boolean result;
if (mode == NuSMVMode.BMC) {
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(nextinstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
nextinstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
} else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
}
Boolean result = getResult(nextinstance, fileno);
if (result) {
System.out.println("Found counter example in step " + (fileno));
......@@ -385,8 +390,8 @@ public class RolesAbsRefine {
rdeptree.addRole(strRole, 0);
while (!vWorkQueue.isEmpty()) {
String strNextRole = vWorkQueue.firstElement(); // Get first element
// from queue.
String strNextRole = vWorkQueue.firstElement();// Get first element
// from queue.
vWorkQueue.remove(strNextRole);
Vector<String> vTmpPosDeps = new Vector<String>();
......@@ -443,6 +448,10 @@ public class RolesAbsRefine {
}
}
public RBACInstance getInputRBACInstance() {
return unsliced;
}
private RoleDepTree rdeptree;
private RBACInstance unsliced;
private RBACInstance nextinstance;
......@@ -465,5 +474,5 @@ public class RolesAbsRefine {
private String strRole;
private int k;
private int lastpriority;
private NuSMVMode mode; // mode
private NuSMVMode mode;// mode
}
src/mohawk/testing/TestRunner.java
View file @ 8df1fdc7
package mohawk.testing;
import java.util.concurrent.Callable;
import java.util.logging.Logger;
import mohawk.global.results.ExecutionResult;
import mohawk.refine.RolesAbsRefine;
public class TestRunner implements Callable<ExecutionResult> {
RolesAbsRefine absrefine;
public final static Logger logger = Logger.getLogger("mohawk");
public TestRunner(RolesAbsRefine absrefine) {
public RolesAbsRefine absrefine = null;
public Boolean skipRefine = false;
public TestRunner(RolesAbsRefine absrefine, boolean skipRefine) {
this.absrefine = absrefine;
this.skipRefine = skipRefine;
}
@Override
public ExecutionResult call() throws Exception {
ExecutionResult result = absrefine.absrefineloop();
ExecutionResult result = null;
if (skipRefine) {
logger.info("[TestRunner] Skipping the Abstraction-Refinement Step");
Boolean counterExampleFound = absrefine.getResult(absrefine.getInputRBACInstance(), 1);
if (counterExampleFound) {
result = ExecutionResult.GOAL_REACHABLE;
} else {
result = ExecutionResult.GOAL_UNREACHABLE;
}
} else {
logger.info("[TestRunner] Running the Abstraction-Refinement Step");
result = absrefine.absrefineloop();
}
return result;
}
......
src/mohawk/testing/TestingSuite.java
View file @ 8df1fdc7
package mohawk.testing;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.io.StringWriter;
......@@ -18,6 +19,7 @@ import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
import mohawk.global.results.ExecutionResult;
import mohawk.global.results.MohawkResults;
import mohawk.global.results.TestingResult;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.math.CalculateDiameter;
......@@ -48,6 +50,11 @@ public class TestingSuite {
*/
public boolean sliceRBACQuery = false;
/**
* Flag for skipping the abstraction-refinement step
*/
public boolean skipRefine = false;
public TestingSuite(SMVSpecHelper smvHelper, MohawkResults results, MohawkTiming timing) {
this.smvHelper = smvHelper;
this.results = results;
......@@ -58,16 +65,19 @@ public class TestingSuite {
public Boolean done() {
this.timing.stopTimer("totalTime");
File results = new File(timingResultsFile);
boolean error = false;
File timingResults = new File(timingResultsFile);
try {
this.timing.writeOut(results);
this.timing.writeOut(timingResults);
} catch (IOException e) {
logger.warning("[TIMING] Unable to save the Timing Results to the file: " + results.getAbsolutePath());
return false;
logger.warning(
"[TIMING] Unable to save the Timing Results to the file: " + timingResults.getAbsolutePath());
error = true;
}
logger.info("[TIMING] Saved Timing Results to the file: " + timingResults.getAbsolutePath());
logger.info("[TIMING] Saved Timing Results to the file: " + results.getAbsolutePath());
return true;
return !error;
}
/**
......@@ -79,6 +89,13 @@ public class TestingSuite {
public void runTests() throws IOException {
logger.entering(getClass().getName(), "runTests()");
FileWriter resultsFW = results.getFileWriter(new File(testingResultsFile), false);
if (resultsFW == null) {
logger.severe("[runTests] Unable to Create, or Write in, the results file: " + testingResultsFile);
throw new IOException("Unable to Create, or Write in, the results file: " + testingResultsFile);
}
ArrayList<NuSMVMode> modes = new ArrayList<NuSMVMode>();
switch (smvHelper.mode) {
case 3:// Both
......@@ -111,6 +128,7 @@ public class TestingSuite {
/* TIMING */timing.startTimer(timerName);
logger.info("Working on " + timerName);
System.out.println("---\n" + "Working on " + timerName);
RBACSpecReader reader = new RBACSpecReader(specFile);
RBACInstance rbac = reader.getRBAC();
......@@ -152,7 +170,7 @@ public class TestingSuite {
absrefine.setMode(modes.get(j));
// Setup Timeout Timer
Future<ExecutionResult> future = executor.submit(new TestRunner(absrefine));
Future<ExecutionResult> future = executor.submit(new TestRunner(absrefine, skipRefine));
try {
logger.info("[RUNNING] Running Mohawk on testcase " + i + "/" + numSpecFiles + " (mode="
+ modes.get(j) + "):");
......@@ -167,6 +185,10 @@ public class TestingSuite {
+ modes.get(j) + "): " + specFile);
/* TIMING */timing.stopTimer(timerName);
results.