From 937cb5b8cb9fe82036d951a834566dfa73501f45 Mon Sep 17 00:00:00 2001
From: rschoene <rene.schoene@tu-dresden.de>
Date: Fri, 29 Nov 2019 18:11:51 +0100
Subject: [PATCH] Add more analyses and the transformation.
---
statemachine.base/build.gradle | 3 +-
.../src/main/jastadd/Analysis.jrag | 51 ++++++++
.../src/main/jastadd/Printing.jrag | 2 +-
.../main/jastadd/StateMachineParser.parser | 9 ++
.../inf/st/statemachine/AnalysisTest.java | 116 ++++++++++++++++++
statemachine.base/src/test/resources/empty.sm | 7 ++
6 files changed, 186 insertions(+), 2 deletions(-)
create mode 100644 statemachine.base/src/test/java/de/tudresden/inf/st/statemachine/AnalysisTest.java
create mode 100644 statemachine.base/src/test/resources/empty.sm
diff --git a/statemachine.base/build.gradle b/statemachine.base/build.gradle
index 9657cfb..fc5b063 100644
--- a/statemachine.base/build.gradle
+++ b/statemachine.base/build.gradle
@@ -131,7 +131,8 @@ jastadd {
scanner.genDir = "src/gen/java/de/tudresden/inf/st/statemachine/jastadd/scanner"
parser.genDir = "src/gen/java/de/tudresden/inf/st/statemachine/jastadd/parser"
- extraJastAddOptions = ['--List=JastAddList']
+// default options are: '--rewrite=cnta', '--safeLazy', '--visitCheck=false', '--cacheCycle=false'
+ extraJastAddOptions = ['--List=JastAddList', '--incremental=param']
}
// Workflow configuration for phases
diff --git a/statemachine.base/src/main/jastadd/Analysis.jrag b/statemachine.base/src/main/jastadd/Analysis.jrag
index fd38416..19eb894 100644
--- a/statemachine.base/src/main/jastadd/Analysis.jrag
+++ b/statemachine.base/src/main/jastadd/Analysis.jrag
@@ -47,4 +47,55 @@ aspect Analysis {
this.getInitial().reachableWithin(this.states().size()).contains(finalState));
}
}
+
+ // --- new ---
+
+ syn int State.minDistTo(State other) circular [-1] {
+ if (this == other) {
+ return 0;
+ }
+ int result = -1;
+ for (Transition t : this.getOutgoingList()) {
+ int dist = t.getTo().minDistTo(other);
+ int delta = t.getLabel().isEmpty() ? 0 : 1;
+ if (dist != -1 && (result == -1 || result > dist + delta)) {
+ result = dist + delta;
+ }
+ }
+ return result;
+ }
+
+ syn boolean Transition.isEpsilon() = getLabel().isEmpty();
+
+ coll Set<Transition> StateMachine.epsilonTransitions() [new HashSet<>()];
+ Transition contributes this when isEpsilon() to StateMachine.epsilonTransitions();
+
+ public void StateMachine.removeEpsilonTransition(Transition t) {
+ if (t.isEpsilon()) {
+ State oldFrom = t.getFrom();
+ State oldTo = t.getTo();
+ if (oldFrom != oldTo) {
+ State combined = new State();
+ combined.setLabel(oldFrom.getLabel() + "+" + oldTo.getLabel());
+ if (oldFrom.isInitial() || oldTo.isInitial()) {
+ this.setInitial(combined);
+ }
+ if (oldFrom.isFinal() || oldTo.isFinal()) {
+ this.addFinal(combined);
+ }
+ new ArrayList<>(oldFrom.getIncomingList()).forEach(trans -> trans.setTo(combined));
+ new ArrayList<>(oldFrom.getOutgoingList()).forEach(trans -> trans.setFrom(combined));
+ new ArrayList<>(oldTo.getIncomingList()).forEach(trans -> trans.setTo(combined));
+ new ArrayList<>(oldTo.getOutgoingList()).forEach(trans -> trans.setFrom(combined));
+ this.removeFinal(oldFrom);
+ this.removeFinal(oldTo);
+ oldFrom.removeSelf();
+ oldTo.removeSelf();
+ this.addElement(combined);
+ }
+ t.removeSelf();
+ } else {
+ System.err.println("Won't remove non-epsilon transition " + t.getLabel());
+ }
+ }
}
diff --git a/statemachine.base/src/main/jastadd/Printing.jrag b/statemachine.base/src/main/jastadd/Printing.jrag
index 5f511fc..1ac2e38 100644
--- a/statemachine.base/src/main/jastadd/Printing.jrag
+++ b/statemachine.base/src/main/jastadd/Printing.jrag
@@ -8,5 +8,5 @@ aspect Printing {
syn String Element.prettyPrint();
eq State.prettyPrint() = (isInitial() ? "initial " : "") + (isFinal() ? "final " : "") + "state " + getLabel() + ";\n";
- eq Transition.prettyPrint() = "trans " + getFrom().getLabel() + " -> " + getTo().getLabel() + " : " + getLabel() + ";\n";
+ eq Transition.prettyPrint() = "trans " + getFrom().getLabel() + " -> " + getTo().getLabel() + (isEpsilon() ? "" : " : " + getLabel()) + ";\n";
}
diff --git a/statemachine.base/src/main/jastadd/StateMachineParser.parser b/statemachine.base/src/main/jastadd/StateMachineParser.parser
index 361e117..e31987a 100644
--- a/statemachine.base/src/main/jastadd/StateMachineParser.parser
+++ b/statemachine.base/src/main/jastadd/StateMachineParser.parser
@@ -22,6 +22,7 @@ statemachine goal =
StateMachine result = new StateMachine(element_list);
result.setInitial(initial);
finals.forEach( result::addFinal );
+ result.treeResolveAll();
return result;
:}
;
@@ -44,6 +45,14 @@ Element element =
result.setTo(State.createRef(to));
return result;
:}
+ | TRANS NAME.from ARROW NAME.to SEMI
+ {:
+ Transition result = new Transition();
+ result.setLabel(""); // epsilon transition
+ result.setFrom(State.createRef(from));
+ result.setTo(State.createRef(to));
+ return result;
+ :}
;
State state_body =
diff --git a/statemachine.base/src/test/java/de/tudresden/inf/st/statemachine/AnalysisTest.java b/statemachine.base/src/test/java/de/tudresden/inf/st/statemachine/AnalysisTest.java
new file mode 100644
index 0000000..28969a5
--- /dev/null
+++ b/statemachine.base/src/test/java/de/tudresden/inf/st/statemachine/AnalysisTest.java
@@ -0,0 +1,116 @@
+package de.tudresden.inf.st.statemachine;
+
+import beaver.Parser;
+import de.tudresden.inf.st.statemachine.jastadd.model.State;
+import de.tudresden.inf.st.statemachine.jastadd.model.StateMachine;
+import de.tudresden.inf.st.statemachine.jastadd.model.Transition;
+import org.junit.Test;
+
+import java.io.IOException;
+import java.nio.file.Paths;
+import java.util.Set;
+
+import static org.junit.Assert.assertEquals;
+
+/**
+ * Testing analysis attributes.
+ *
+ * @author rschoene - Initial contribution
+ */
+public class AnalysisTest {
+
+ @Test
+ public void test1() throws IOException, Parser.Exception {
+ StateMachine stateMachine = ParserUtils.load(Paths.get("src", "test", "resources", "machine_one.sm"));
+ State s = stateMachine.globallyResolveStateByToken("S");
+ State a = stateMachine.globallyResolveStateByToken("A");
+ State e = stateMachine.globallyResolveStateByToken("E");
+
+ assertEquals(0, s.minDistTo(s));
+ assertEquals(1, s.minDistTo(a));
+ assertEquals(2, s.minDistTo(e));
+ assertEquals(1, a.minDistTo(e));
+ assertEquals(1, a.minDistTo(s));
+ assertEquals(0, a.minDistTo(a));
+ assertEquals(-1, e.minDistTo(s));
+ assertEquals(-1, e.minDistTo(a));
+ assertEquals(0, e.minDistTo(e));
+ }
+
+ @Test
+ public void testEmpty() throws IOException, Parser.Exception {
+ StateMachine stateMachine = ParserUtils.load(Paths.get("src", "test", "resources", "empty.sm"));
+
+ State s = stateMachine.globallyResolveStateByToken("S");
+ State a = stateMachine.globallyResolveStateByToken("A");
+ State e = stateMachine.globallyResolveStateByToken("E");
+
+ assertEquals(0, s.minDistTo(s));
+ assertEquals(1, s.minDistTo(a));
+ assertEquals(2, s.minDistTo(e));
+ assertEquals(1, a.minDistTo(e));
+ assertEquals(1, a.minDistTo(s));
+ assertEquals(0, a.minDistTo(a));
+ assertEquals(-1, e.minDistTo(s));
+ assertEquals(-1, e.minDistTo(a));
+ assertEquals(0, e.minDistTo(e));
+
+ // change some things
+ Transition t5 = new Transition();
+ t5.setFrom(a);
+ t5.setTo(e);
+ stateMachine.addElement(t5);
+
+ System.out.println(stateMachine.prettyPrint());
+
+ assertEquals(0, s.minDistTo(s));
+ assertEquals(1, s.minDistTo(a));
+ assertEquals(1, s.minDistTo(e));
+ assertEquals(0, a.minDistTo(e));
+ assertEquals(1, a.minDistTo(s));
+ assertEquals(0, a.minDistTo(a));
+ assertEquals(-1, e.minDistTo(s));
+ assertEquals(-1, e.minDistTo(a));
+ assertEquals(0, e.minDistTo(e));
+
+ Set<Transition> epsilons = stateMachine.epsilonTransitions();
+ assertEquals(2, epsilons.size());
+
+ for (Transition eps : epsilons) {
+ removeEpsilonTransition(stateMachine, eps);
+ }
+
+ State ae = stateMachine.globallyResolveStateByToken("A+E");
+ Transition t6 = new Transition();
+ t6.setFrom(s);
+ t6.setTo(ae);
+ stateMachine.addElement(t6);
+
+ System.out.println(stateMachine.prettyPrint());
+
+ epsilons = stateMachine.epsilonTransitions();
+ assertEquals(1, epsilons.size());
+
+ for (Transition eps : epsilons) {
+ removeEpsilonTransition(stateMachine, eps);
+ }
+ }
+
+ private void removeEpsilonTransition(StateMachine stateMachine, Transition eps) {
+ System.out.print("removing epsilon transition " + eps.prettyPrint());
+ System.out.println("Minimal distances before:");
+ initialToFinalDists(stateMachine);
+ stateMachine.removeEpsilonTransition(eps);
+ System.out.println("Minimal distances after:");
+ initialToFinalDists(stateMachine);
+ System.out.println("StateMachine after");
+ System.out.println(stateMachine.prettyPrint());
+ }
+
+ private void initialToFinalDists(StateMachine stateMachine) {
+ for (State finalState : stateMachine.getFinalList()) {
+ System.out.println("initial state "+ stateMachine.getInitial() + " to " + finalState + " in " +
+ stateMachine.getInitial().minDistTo(finalState) + " step(s)");
+ }
+ }
+}
diff --git a/statemachine.base/src/test/resources/empty.sm b/statemachine.base/src/test/resources/empty.sm
new file mode 100644
index 0000000..1bbcce6
--- /dev/null
+++ b/statemachine.base/src/test/resources/empty.sm
@@ -0,0 +1,7 @@
+initial state S;
+state A;
+final state E;
+trans S -> A : t1;
+trans A -> S : t2;
+trans A -> A;
+trans A -> E : t3;
--
GitLab