From 53d08fabbe4bd5cfb4a018fe4338a544cf7fa64c Mon Sep 17 00:00:00 2001 From: Thomas Lohse Date: Thu, 1 Dec 2022 11:19:52 +0100 Subject: [PATCH 1/5] Initial rename --- samples/xml/BoolQuotient.xml | 2 +- samples/xml/ConsTests.xml | 2 +- samples/xml/DisjunctionTests.xml | 2 +- samples/xml/ImplTests.xml | 2 +- samples/xml/bisimilarity.xml | 10 +- samples/xml/booleanRefinement.xml | 18 +- samples/xml/booleanRefinementOneAut.xml | 4 +- samples/xml/conjun.xml | 2 +- samples/xml/delayRefinement.xml | 76 +++--- samples/xml/is_consistent_single.xml | 2 +- samples/xml/misc_test.xml | 2 +- samples/xml/quotient/QuotientTestOutputs.xml | 52 ++-- .../quotient/SimpleTimedQuotientTest02.xml | 52 ++-- ...ritical_sections_final_versions_pruned.xml | 2 +- samples/xml/quotient/pruningWithOr.xml | 48 ++-- samples/xml/quotient/pruningWithOrOnlyOne.xml | 8 +- .../quotient/pruningWithOrOnlyOriginal.xml | 4 +- samples/xml/quotient/simple3NoDiagonal.xml | 4 +- samples/xml/refinement_bool.xml | 16 +- samples/xml/selfloopNonZeno.xml | 2 +- samples/xml/simple.xml | 2 +- samples/xml/simpliversity.xml | 2 +- samples/xml/staticSpecDIVAdm.xml | 166 ++++++------ samples/xml/test.xml | 8 +- samples/xml/test1.txt | 8 +- samples/xml/test1.xml | 8 +- samples/xml/timedInconsistency.xml | 20 +- samples/xml/timedReach.xml | 4 +- samples/xml/university-is-getting-simpler.xml | 12 +- samples/xml/university-slice.xml | 2 +- samples/xml/university-universalSpec.xml | 12 +- samples/xml/university.xml | 2 +- .../{GuardGrammar.g4 => ExpressionGrammar.g4} | 10 +- src/logic/AggregatedTransitionSystem.java | 4 +- src/logic/Bisimilarity.java | 2 +- src/logic/JsonAutomatonEncoder.java | 2 +- src/logic/Pruning.java | 42 +-- src/logic/SimpleTransitionSystem.java | 14 +- src/logic/State.java | 6 +- src/logic/StatePair.java | 6 +- src/logic/Transition.java | 2 +- src/models/AndExpression.java | 126 +++++++++ src/models/AndGuard.java | 126 --------- src/models/Automaton.java | 8 +- .../{BoolGuard.java => BoolExpression.java} | 26 +- src/models/CDD.java | 78 +++--- .../{ClockGuard.java => ClockExpression.java} | 26 +- src/models/Edge.java | 28 +- src/models/{Guard.java => Expression.java} | 14 +- .../{FalseGuard.java => FalseExpression.java} | 8 +- src/models/Federation.java | 8 +- src/models/Location.java | 60 ++--- src/models/Move.java | 4 +- src/models/OrExpression.java | 127 +++++++++ src/models/OrGuard.java | 127 --------- .../{TrueGuard.java => TrueExpression.java} | 8 +- src/models/Zone.java | 38 +-- src/parser/ExpressionParser.java | 106 ++++++++ src/parser/GuardParser.java | 106 -------- src/parser/JSONParser.java | 10 +- src/parser/XMLFileWriter.java | 2 +- src/parser/XMLParser.java | 10 +- test/cdd/CDDTest.java | 34 +-- test/dbm/DBMTest.java | 24 +- test/features/BoolTest.java | 240 +++++++++--------- test/models/AutomatonTest.java | 14 +- test/models/DisjunctionTest.java | 32 +-- .../{GuardTest.java => ExpressionTest.java} | 10 +- test/models/InputEnablednessTest.java | 80 +++--- test/models/VariousTest.java | 34 +-- ...arTest.java => ExpressionGrammarTest.java} | 2 +- ...serTest.java => ExpressionParserTest.java} | 38 +-- test/parser/JSONParserTest.java | 87 +++---- test/parser/XMLParserTest.java | 19 +- 74 files changed, 1150 insertions(+), 1154 deletions(-) rename src/antlr/{GuardGrammar.g4 => ExpressionGrammar.g4} (73%) create mode 100644 src/models/AndExpression.java delete mode 100644 src/models/AndGuard.java rename src/models/{BoolGuard.java => BoolExpression.java} (67%) rename src/models/{ClockGuard.java => ClockExpression.java} (79%) rename src/models/{Guard.java => Expression.java} (57%) rename src/models/{FalseGuard.java => FalseExpression.java} (61%) create mode 100644 src/models/OrExpression.java delete mode 100644 src/models/OrGuard.java rename src/models/{TrueGuard.java => TrueExpression.java} (61%) create mode 100644 src/parser/ExpressionParser.java delete mode 100644 src/parser/GuardParser.java rename test/models/{GuardTest.java => ExpressionTest.java} (68%) rename test/parser/{GuardGrammarTest.java => ExpressionGrammarTest.java} (99%) rename test/parser/{GuardParserTest.java => ExpressionParserTest.java} (60%) diff --git a/samples/xml/BoolQuotient.xml b/samples/xml/BoolQuotient.xml index 524615d4..d943313a 100644 --- a/samples/xml/BoolQuotient.xml +++ b/samples/xml/BoolQuotient.xml @@ -23,7 +23,7 @@ bool f=false; - + diff --git a/samples/xml/ConsTests.xml b/samples/xml/ConsTests.xml index f7e172b3..e1d332cd 100644 --- a/samples/xml/ConsTests.xml +++ b/samples/xml/ConsTests.xml @@ -1,5 +1,5 @@ // Place global declarations here. -broadcast chan i, o;// Place template instantiations here. +broadcast chan i, o;// Place template instantiations here. // List one or more processes to be composed into a system. system G1, G2, G3, G4, G5, G6, G7, G8, G9, G10, diff --git a/samples/xml/DisjunctionTests.xml b/samples/xml/DisjunctionTests.xml index 6d0e015c..bad4436b 100644 --- a/samples/xml/DisjunctionTests.xml +++ b/samples/xml/DisjunctionTests.xml @@ -1,7 +1,7 @@ // Place global declarations here. chan i; system D1,D2; +clock x;system D1,D2; IO D1 { i? } IO D2 { i? } diff --git a/samples/xml/ImplTests.xml b/samples/xml/ImplTests.xml index 1148ed0e..08b45f58 100644 --- a/samples/xml/ImplTests.xml +++ b/samples/xml/ImplTests.xml @@ -1,5 +1,5 @@ // Place global declarations here. -broadcast chan i, o;// Place template instantiations here. +broadcast chan i, o;// Place template instantiations here. // List one or more processes to be composed into a system. system Test, G1, G2, G3, G4, G5, G6, G7, G8, G9, G10, diff --git a/samples/xml/bisimilarity.xml b/samples/xml/bisimilarity.xml index 54719a44..8a236518 100644 --- a/samples/xml/bisimilarity.xml +++ b/samples/xml/bisimilarity.xml @@ -46,7 +46,7 @@ clock x, y; - + @@ -54,19 +54,19 @@ clock x, y; - + - + - + @@ -77,7 +77,7 @@ clock x, y; - + diff --git a/samples/xml/booleanRefinement.xml b/samples/xml/booleanRefinement.xml index 3611413b..3cf1837a 100644 --- a/samples/xml/booleanRefinement.xml +++ b/samples/xml/booleanRefinement.xml @@ -42,13 +42,13 @@ bool a=false; - + - + @@ -70,7 +70,7 @@ bool a=false; - + @@ -79,7 +79,7 @@ bool a=false; - + @@ -110,7 +110,7 @@ bool a = false; - + @@ -118,7 +118,7 @@ bool a = false; - + @@ -126,7 +126,7 @@ bool a = false; - + @@ -135,13 +135,13 @@ bool a = false; - + - + diff --git a/samples/xml/booleanRefinementOneAut.xml b/samples/xml/booleanRefinementOneAut.xml index 538102cd..f13bdd4d 100644 --- a/samples/xml/booleanRefinementOneAut.xml +++ b/samples/xml/booleanRefinementOneAut.xml @@ -18,7 +18,7 @@ bool a=false; - + @@ -27,7 +27,7 @@ bool a=false; - + diff --git a/samples/xml/conjun.xml b/samples/xml/conjun.xml index ae6f41cd..da1124d9 100644 --- a/samples/xml/conjun.xml +++ b/samples/xml/conjun.xml @@ -2,7 +2,7 @@ broadcast chan i, o, o1, i1, o2,k, go;// Place template instantiations here. +// Place template instantiations here. // List one or more processes to be composed into a system. system P0, P1, P2, P3, P4, P5, P6, P7, P8,P9,P10,P11,P12,P13; diff --git a/samples/xml/delayRefinement.xml b/samples/xml/delayRefinement.xml index b41db45b..df061077 100644 --- a/samples/xml/delayRefinement.xml +++ b/samples/xml/delayRefinement.xml @@ -276,7 +276,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -354,7 +354,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -746,13 +746,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -770,13 +770,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -795,13 +795,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -820,13 +820,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -851,7 +851,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -874,7 +874,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -891,13 +891,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -914,13 +914,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -937,13 +937,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -960,13 +960,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -997,7 +997,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1024,7 +1024,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1032,7 +1032,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1049,14 +1049,14 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -1076,20 +1076,20 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + - + @@ -1107,7 +1107,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1127,7 +1127,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1142,7 +1142,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1167,13 +1167,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -1198,13 +1198,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + @@ -1219,7 +1219,7 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + @@ -1236,13 +1236,13 @@ broadcast chan ri, ro, i, o, rand, n1, n2, err1, err2, go, dio, - + - + diff --git a/samples/xml/is_consistent_single.xml b/samples/xml/is_consistent_single.xml index 4653d16e..68775d83 100644 --- a/samples/xml/is_consistent_single.xml +++ b/samples/xml/is_consistent_single.xml @@ -16,7 +16,7 @@ clock y; - + diff --git a/samples/xml/misc_test.xml b/samples/xml/misc_test.xml index 677e017f..f0ad2df1 100644 --- a/samples/xml/misc_test.xml +++ b/samples/xml/misc_test.xml @@ -13,7 +13,7 @@ clock x; - + diff --git a/samples/xml/quotient/QuotientTestOutputs.xml b/samples/xml/quotient/QuotientTestOutputs.xml index bbf9ff69..e509f85e 100644 --- a/samples/xml/quotient/QuotientTestOutputs.xml +++ b/samples/xml/quotient/QuotientTestOutputs.xml @@ -18,7 +18,7 @@ clock x,y; - + @@ -26,7 +26,7 @@ clock x,y; - + @@ -41,7 +41,7 @@ clock x,y; - + @@ -59,7 +59,7 @@ clock x,y; - + @@ -68,7 +68,7 @@ clock x,y; - + @@ -82,7 +82,7 @@ clock x,y; - + @@ -110,13 +110,13 @@ clock x,y; - + - + @@ -134,13 +134,13 @@ clock x,y; - + - + @@ -164,14 +164,14 @@ clock x,y; - + - + @@ -188,13 +188,13 @@ clock x,y; - + - + @@ -216,13 +216,13 @@ clock x,y; - + - + @@ -245,13 +245,13 @@ clock x,y; - + - + @@ -272,13 +272,13 @@ clock x,y; - + - + @@ -332,13 +332,13 @@ clock x,y; - + - + @@ -372,13 +372,13 @@ clock x,y; - + - + @@ -402,13 +402,13 @@ clock x,y; - + - + diff --git a/samples/xml/quotient/SimpleTimedQuotientTest02.xml b/samples/xml/quotient/SimpleTimedQuotientTest02.xml index ee035046..64301344 100644 --- a/samples/xml/quotient/SimpleTimedQuotientTest02.xml +++ b/samples/xml/quotient/SimpleTimedQuotientTest02.xml @@ -38,7 +38,7 @@ clock z; - + @@ -46,7 +46,7 @@ clock z; - + @@ -54,7 +54,7 @@ clock z; - + @@ -90,35 +90,35 @@ clock z; - + - + - + - + - + @@ -132,7 +132,7 @@ clock z; - + @@ -140,7 +140,7 @@ clock z; - + @@ -148,7 +148,7 @@ clock z; - + @@ -184,7 +184,7 @@ clock z; - + @@ -192,7 +192,7 @@ clock z; - + @@ -204,7 +204,7 @@ clock z; - + @@ -212,7 +212,7 @@ clock z; - + @@ -220,7 +220,7 @@ clock z; - + @@ -256,42 +256,42 @@ clock z; - + - + - + - + - + - + @@ -299,7 +299,7 @@ clock z; - + @@ -312,7 +312,7 @@ clock z; - + @@ -320,7 +320,7 @@ clock z; - + @@ -328,7 +328,7 @@ clock z; - + diff --git a/samples/xml/quotient/example_critical_sections_final_versions_pruned.xml b/samples/xml/quotient/example_critical_sections_final_versions_pruned.xml index 5e5d9e81..5749748d 100644 --- a/samples/xml/quotient/example_critical_sections_final_versions_pruned.xml +++ b/samples/xml/quotient/example_critical_sections_final_versions_pruned.xml @@ -614,7 +614,7 @@ broadcast chan i[N], c[N], g[N]; - + diff --git a/samples/xml/quotient/pruningWithOr.xml b/samples/xml/quotient/pruningWithOr.xml index 9241f4da..81e02b05 100644 --- a/samples/xml/quotient/pruningWithOr.xml +++ b/samples/xml/quotient/pruningWithOr.xml @@ -20,7 +20,7 @@ clock x; - + @@ -31,7 +31,7 @@ clock x; - + @@ -49,13 +49,13 @@ clock x; - + - + @@ -76,7 +76,7 @@ clock x; - + @@ -87,7 +87,7 @@ clock x; - + @@ -106,13 +106,13 @@ clock x; - + - + @@ -134,7 +134,7 @@ bool a,b; - + @@ -145,7 +145,7 @@ bool a,b; - + @@ -167,13 +167,13 @@ x>=10) - + - - + - + -