From 7b3c1193e94c87776bb8c5485720186e5d0b90f4 Mon Sep 17 00:00:00 2001
From: Johannes Mey <johannes.mey@tu-dresden.de>
Date: Mon, 2 Dec 2019 00:45:38 +0100
Subject: [PATCH] add some comments, remove complicated additional analysis
from task
---
.../src/main/jastadd/Analysis.jadd | 21 ++++++++
.../src/main/jastadd/Analysis.jrag | 51 ++-----------------
.../src/main/jastadd/NameAnalysis.jrag | 3 ++
.../src/main/jastadd/Navigation.jrag | 11 ++++
.../src/main/jastadd/Printing.jrag | 3 ++
.../src/main/jastadd/Transformation.jadd | 32 ++++++++++++
.../src/main/jastadd/Util.jrag | 3 --
.../src/main/jastadd/Analysis.jadd | 14 +++++
.../src/main/jastadd/Analysis.jrag | 51 ++-----------------
.../src/main/jastadd/ConnectedComponents.jrag | 37 --------------
.../src/main/jastadd/NameAnalysis.jrag | 3 ++
.../src/main/jastadd/Navigation.jrag | 11 ++++
.../src/main/jastadd/Printing.jrag | 3 ++
.../src/main/jastadd/SMtoDotG.jrag | 18 -------
.../src/main/jastadd/Transformation.jadd | 32 ++++++++++++
statemachine.task/src/main/jastadd/Util.jrag | 3 --
.../tudresden/inf/st/statemachine/Main.java | 2 -
17 files changed, 143 insertions(+), 155 deletions(-)
create mode 100644 statemachine.solution/src/main/jastadd/Analysis.jadd
create mode 100644 statemachine.solution/src/main/jastadd/Transformation.jadd
delete mode 100644 statemachine.solution/src/main/jastadd/Util.jrag
create mode 100644 statemachine.task/src/main/jastadd/Analysis.jadd
delete mode 100644 statemachine.task/src/main/jastadd/ConnectedComponents.jrag
delete mode 100644 statemachine.task/src/main/jastadd/SMtoDotG.jrag
create mode 100644 statemachine.task/src/main/jastadd/Transformation.jadd
delete mode 100644 statemachine.task/src/main/jastadd/Util.jrag
diff --git a/statemachine.solution/src/main/jastadd/Analysis.jadd b/statemachine.solution/src/main/jastadd/Analysis.jadd
new file mode 100644
index 0000000..a7d363f
--- /dev/null
+++ b/statemachine.solution/src/main/jastadd/Analysis.jadd
@@ -0,0 +1,21 @@
+aspect Analysis {
+
+ public void StateMachine.printSomeAnalysis() {
+ Set<Set<State>> sccs = this.SCC();
+ System.out.print("SCCs found: ");
+ for (Set<State> scc : sccs) {
+ System.out.print(scc + " ");
+ }
+ System.out.println();
+
+ for (State s : this.states()) {
+ System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable());
+ }
+
+ for (State finalState : this.getFinalList()) {
+ System.out.println("initial state "+ this.getInitial() + " to " + finalState + " in " +
+ this.getInitial().minDistTo(finalState) + " step(s)");
+ }
+ }
+
+}
diff --git a/statemachine.solution/src/main/jastadd/Analysis.jrag b/statemachine.solution/src/main/jastadd/Analysis.jrag
index 6bbcf6a..4bc4a05 100644
--- a/statemachine.solution/src/main/jastadd/Analysis.jrag
+++ b/statemachine.solution/src/main/jastadd/Analysis.jrag
@@ -1,4 +1,6 @@
aspect Analysis {
+
+ /** Compute all states reachable from the current state */
syn Set<State> State.reachable() circular [new HashSet<State>()] {
Set<State> result = new HashSet<>();
result.addAll(successors());
@@ -8,24 +10,7 @@ aspect Analysis {
return result;
}
- public void StateMachine.printSomeAnalysis() {
- Set<Set<State>> sccs = this.SCC();
- System.out.print("SCCs found: ");
- for (Set<State> scc : sccs) {
- System.out.print(scc + " ");
- }
- System.out.println();
-
- for (State s : this.states()) {
- System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable());
- }
-
- for (State finalState : this.getFinalList()) {
- System.out.println("initial state "+ this.getInitial() + " to " + finalState + " in " +
- this.getInitial().minDistTo(finalState) + " step(s)");
- }
- }
-
+ /** Compute the minimum number of transitions to the other state, ignoring states with empty labels */
syn int State.minDistTo(State other) circular [-1] {
if (this == other) {
return 0;
@@ -41,37 +26,11 @@ aspect Analysis {
return result;
}
+ /** A transition is an epsilon transition if the label is empty */
syn boolean Transition.isEpsilon() = getLabel().isEmpty();
+ /** Collect all epsilon transitions */
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.solution/src/main/jastadd/NameAnalysis.jrag b/statemachine.solution/src/main/jastadd/NameAnalysis.jrag
index ddd0f07..12adfd3 100644
--- a/statemachine.solution/src/main/jastadd/NameAnalysis.jrag
+++ b/statemachine.solution/src/main/jastadd/NameAnalysis.jrag
@@ -1,4 +1,6 @@
aspect NameAnalysis {
+
+ /** resolve a state using its name */
syn State StateMachine.resolveState(String id) {
for (State s : states()) {
if (s.getLabel().equals(id)) {
@@ -8,6 +10,7 @@ aspect NameAnalysis {
return null;
}
+ /** resolve a transition using its name */
syn Transition StateMachine.resolveTransition(String id) {
for (Transition t : transitions()) {
if (t.getLabel().equals(id)) {
diff --git a/statemachine.solution/src/main/jastadd/Navigation.jrag b/statemachine.solution/src/main/jastadd/Navigation.jrag
index f06ecb8..18c4e4f 100644
--- a/statemachine.solution/src/main/jastadd/Navigation.jrag
+++ b/statemachine.solution/src/main/jastadd/Navigation.jrag
@@ -1,5 +1,9 @@
aspect Navigation {
+ // ======================================================
+ // Atributes to complete
+ // ======================================================
+
/** Check, whether an this element is a state */
syn boolean Element.isState() = false;
eq State.isState() = true;
@@ -27,6 +31,7 @@ aspect Navigation {
return states;
}
+ /** Get all transitions */
syn List<Transition> StateMachine.transitions() {
List<Transition> transitions = new ArrayList<>();
for (Element element: getElementList()) {
@@ -37,11 +42,17 @@ aspect Navigation {
return transitions;
}
+ /** Get the state machine the element is contained in */
inh StateMachine Element.containingStateMachine();
eq StateMachine.getElement().containingStateMachine() = this;
+ /** Determine whether the State is final */
syn boolean State.isInitial() = containingStateMachine().getInitial().equals(this);
+
+ /** Determine whether the State is final */
syn boolean State.isFinal() = containingStateMachine().getFinalList().contains(this);
+ /** Get all successor states */
syn Collection<State> State.successors() = getOutgoingList().stream().map(Transition::getTo).collect(Collectors.toList());
+
}
diff --git a/statemachine.solution/src/main/jastadd/Printing.jrag b/statemachine.solution/src/main/jastadd/Printing.jrag
index 1ac2e38..90df2b9 100644
--- a/statemachine.solution/src/main/jastadd/Printing.jrag
+++ b/statemachine.solution/src/main/jastadd/Printing.jrag
@@ -1,4 +1,6 @@
aspect Printing {
+
+ /** Return a textual representation of the state machine */
syn String StateMachine.prettyPrint() {
StringBuilder sb = new StringBuilder();
states().forEach(s -> sb.append(s.prettyPrint()));
@@ -6,6 +8,7 @@ aspect Printing {
return sb.toString();
}
+ /** Return a textual representation of the state machine */
syn String Element.prettyPrint();
eq State.prettyPrint() = (isInitial() ? "initial " : "") + (isFinal() ? "final " : "") + "state " + getLabel() + ";\n";
eq Transition.prettyPrint() = "trans " + getFrom().getLabel() + " -> " + getTo().getLabel() + (isEpsilon() ? "" : " : " + getLabel()) + ";\n";
diff --git a/statemachine.solution/src/main/jastadd/Transformation.jadd b/statemachine.solution/src/main/jastadd/Transformation.jadd
new file mode 100644
index 0000000..2663294
--- /dev/null
+++ b/statemachine.solution/src/main/jastadd/Transformation.jadd
@@ -0,0 +1,32 @@
+aspect Transformation {
+
+ /** remove transformations with empty labels */
+ 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.solution/src/main/jastadd/Util.jrag b/statemachine.solution/src/main/jastadd/Util.jrag
deleted file mode 100644
index 37592dd..0000000
--- a/statemachine.solution/src/main/jastadd/Util.jrag
+++ /dev/null
@@ -1,3 +0,0 @@
-aspect Util {
-
-}
diff --git a/statemachine.task/src/main/jastadd/Analysis.jadd b/statemachine.task/src/main/jastadd/Analysis.jadd
new file mode 100644
index 0000000..0c9fb01
--- /dev/null
+++ b/statemachine.task/src/main/jastadd/Analysis.jadd
@@ -0,0 +1,14 @@
+aspect Analysis {
+
+ public void StateMachine.printSomeAnalysis() {
+ for (State s : this.states()) {
+ System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable());
+ }
+
+ for (State finalState : this.getFinalList()) {
+ System.out.println("initial state "+ this.getInitial() + " to " + finalState + " in " +
+ this.getInitial().minDistTo(finalState) + " step(s)");
+ }
+ }
+
+}
diff --git a/statemachine.task/src/main/jastadd/Analysis.jrag b/statemachine.task/src/main/jastadd/Analysis.jrag
index 6bbcf6a..4bc4a05 100644
--- a/statemachine.task/src/main/jastadd/Analysis.jrag
+++ b/statemachine.task/src/main/jastadd/Analysis.jrag
@@ -1,4 +1,6 @@
aspect Analysis {
+
+ /** Compute all states reachable from the current state */
syn Set<State> State.reachable() circular [new HashSet<State>()] {
Set<State> result = new HashSet<>();
result.addAll(successors());
@@ -8,24 +10,7 @@ aspect Analysis {
return result;
}
- public void StateMachine.printSomeAnalysis() {
- Set<Set<State>> sccs = this.SCC();
- System.out.print("SCCs found: ");
- for (Set<State> scc : sccs) {
- System.out.print(scc + " ");
- }
- System.out.println();
-
- for (State s : this.states()) {
- System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable());
- }
-
- for (State finalState : this.getFinalList()) {
- System.out.println("initial state "+ this.getInitial() + " to " + finalState + " in " +
- this.getInitial().minDistTo(finalState) + " step(s)");
- }
- }
-
+ /** Compute the minimum number of transitions to the other state, ignoring states with empty labels */
syn int State.minDistTo(State other) circular [-1] {
if (this == other) {
return 0;
@@ -41,37 +26,11 @@ aspect Analysis {
return result;
}
+ /** A transition is an epsilon transition if the label is empty */
syn boolean Transition.isEpsilon() = getLabel().isEmpty();
+ /** Collect all epsilon transitions */
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.task/src/main/jastadd/ConnectedComponents.jrag b/statemachine.task/src/main/jastadd/ConnectedComponents.jrag
deleted file mode 100644
index 1637d45..0000000
--- a/statemachine.task/src/main/jastadd/ConnectedComponents.jrag
+++ /dev/null
@@ -1,37 +0,0 @@
-aspect ConnectedComponents {
-
- /**
- * Kosaraju's algorithm
- */
- syn Set<Set<State>> StateMachine.SCC() {
- Map<State, Set> visited = new HashMap<>();
- LinkedList<State> locked = new LinkedList<>();
-
- for (State n : states())
- if (!visited.containsKey(n))
- n.visit(visited, locked); // forward search
-
- for (State n : locked)
- if (visited.get(n) == null)
- n.assign(visited, new HashSet()); // backward search
-
- return new HashSet(visited.values());
- }
-
- void State.visit(Map<State, Set> visited, LinkedList<State> locked) {
- visited.put(this, null);
- for (Transition t : getOutgoingList())
- if (!visited.containsKey(t.getTo()))
- t.getTo().visit(visited, locked);
- locked.addFirst(this);
- }
-
- void State.assign(Map<State, Set> visited, Set root) {
- root.add(this);
- visited.put(this, root);
- for (Transition t : getIncomingList())
- if (visited.get(t.getFrom()) == null)
- t.getFrom().assign(visited, root);
- }
-
-}
diff --git a/statemachine.task/src/main/jastadd/NameAnalysis.jrag b/statemachine.task/src/main/jastadd/NameAnalysis.jrag
index ddd0f07..12adfd3 100644
--- a/statemachine.task/src/main/jastadd/NameAnalysis.jrag
+++ b/statemachine.task/src/main/jastadd/NameAnalysis.jrag
@@ -1,4 +1,6 @@
aspect NameAnalysis {
+
+ /** resolve a state using its name */
syn State StateMachine.resolveState(String id) {
for (State s : states()) {
if (s.getLabel().equals(id)) {
@@ -8,6 +10,7 @@ aspect NameAnalysis {
return null;
}
+ /** resolve a transition using its name */
syn Transition StateMachine.resolveTransition(String id) {
for (Transition t : transitions()) {
if (t.getLabel().equals(id)) {
diff --git a/statemachine.task/src/main/jastadd/Navigation.jrag b/statemachine.task/src/main/jastadd/Navigation.jrag
index f06ecb8..18c4e4f 100644
--- a/statemachine.task/src/main/jastadd/Navigation.jrag
+++ b/statemachine.task/src/main/jastadd/Navigation.jrag
@@ -1,5 +1,9 @@
aspect Navigation {
+ // ======================================================
+ // Atributes to complete
+ // ======================================================
+
/** Check, whether an this element is a state */
syn boolean Element.isState() = false;
eq State.isState() = true;
@@ -27,6 +31,7 @@ aspect Navigation {
return states;
}
+ /** Get all transitions */
syn List<Transition> StateMachine.transitions() {
List<Transition> transitions = new ArrayList<>();
for (Element element: getElementList()) {
@@ -37,11 +42,17 @@ aspect Navigation {
return transitions;
}
+ /** Get the state machine the element is contained in */
inh StateMachine Element.containingStateMachine();
eq StateMachine.getElement().containingStateMachine() = this;
+ /** Determine whether the State is final */
syn boolean State.isInitial() = containingStateMachine().getInitial().equals(this);
+
+ /** Determine whether the State is final */
syn boolean State.isFinal() = containingStateMachine().getFinalList().contains(this);
+ /** Get all successor states */
syn Collection<State> State.successors() = getOutgoingList().stream().map(Transition::getTo).collect(Collectors.toList());
+
}
diff --git a/statemachine.task/src/main/jastadd/Printing.jrag b/statemachine.task/src/main/jastadd/Printing.jrag
index 1ac2e38..90df2b9 100644
--- a/statemachine.task/src/main/jastadd/Printing.jrag
+++ b/statemachine.task/src/main/jastadd/Printing.jrag
@@ -1,4 +1,6 @@
aspect Printing {
+
+ /** Return a textual representation of the state machine */
syn String StateMachine.prettyPrint() {
StringBuilder sb = new StringBuilder();
states().forEach(s -> sb.append(s.prettyPrint()));
@@ -6,6 +8,7 @@ aspect Printing {
return sb.toString();
}
+ /** Return a textual representation of the state machine */
syn String Element.prettyPrint();
eq State.prettyPrint() = (isInitial() ? "initial " : "") + (isFinal() ? "final " : "") + "state " + getLabel() + ";\n";
eq Transition.prettyPrint() = "trans " + getFrom().getLabel() + " -> " + getTo().getLabel() + (isEpsilon() ? "" : " : " + getLabel()) + ";\n";
diff --git a/statemachine.task/src/main/jastadd/SMtoDotG.jrag b/statemachine.task/src/main/jastadd/SMtoDotG.jrag
deleted file mode 100644
index 18155d5..0000000
--- a/statemachine.task/src/main/jastadd/SMtoDotG.jrag
+++ /dev/null
@@ -1,18 +0,0 @@
-aspect StateMachinetoDotG {
- syn String StateMachine.toDot() {
- StringBuilder b = new StringBuilder();
- b.append("strict digraph cycles {\n");
-
- for (State from : states()) {
- b.append(" ").append(from.getLabel()).append("[label=\"").append(from.getLabel()).append("\"];\n");
-
- for (Transition out : from.getOutgoingList()) {
- b.append(" ").append(from.getLabel()).append(" -> ").append(out.getTo().getLabel())
- .append("[label=\"").append(out.getLabel()).append("\"];\n");
- }
- }
-
- b.append("}\n");
- return b.toString();
- }
-}
diff --git a/statemachine.task/src/main/jastadd/Transformation.jadd b/statemachine.task/src/main/jastadd/Transformation.jadd
new file mode 100644
index 0000000..2663294
--- /dev/null
+++ b/statemachine.task/src/main/jastadd/Transformation.jadd
@@ -0,0 +1,32 @@
+aspect Transformation {
+
+ /** remove transformations with empty labels */
+ 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.task/src/main/jastadd/Util.jrag b/statemachine.task/src/main/jastadd/Util.jrag
deleted file mode 100644
index 37592dd..0000000
--- a/statemachine.task/src/main/jastadd/Util.jrag
+++ /dev/null
@@ -1,3 +0,0 @@
-aspect Util {
-
-}
diff --git a/statemachine.task/src/main/java/de/tudresden/inf/st/statemachine/Main.java b/statemachine.task/src/main/java/de/tudresden/inf/st/statemachine/Main.java
index d38b8ac..cca109b 100644
--- a/statemachine.task/src/main/java/de/tudresden/inf/st/statemachine/Main.java
+++ b/statemachine.task/src/main/java/de/tudresden/inf/st/statemachine/Main.java
@@ -39,8 +39,6 @@ public class Main {
printHeading("StateMachine after");
System.out.println(stateMachine.prettyPrint());
}
- printHeading("DotGraph");
- System.out.println(stateMachine.toDot());
DrAST_root_node = stateMachine;
}
--
GitLab