diff --git a/statemachine.solution/src/main/jastadd/Analysis.jadd b/statemachine.solution/src/main/jastadd/Analysis.jadd new file mode 100644 index 0000000000000000000000000000000000000000..a7d363ffdfead4e117290c5fd33c7990bede775c --- /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 6bbcf6a8b935f93575a52d5d5509ac94df130161..4bc4a0502203c41538702d22c19e2f3fc9caea26 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 ddd0f07e78771883c58a5d86e12dc4e3bafc4479..12adfd31b2629800dca5bc4db829173784b90264 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 f06ecb8dcdf0d7682223ae92deb96b5cfe530696..18c4e4fbf90718c6ebdef69c96053fa054bf09fd 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 1ac2e382cbaf7309b40ffbee3c2b47da1d83ca38..90df2b9e9e74cdc0f3189d096c009b31aba077a8 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 0000000000000000000000000000000000000000..266329489bc477b806aa4ae876a0ca2771a59596 --- /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 37592dd03f23a930f234c96da18e373a8237b311..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..0c9fb018e0f9aed5415b8ec3b3a72b4d675f5a17 --- /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 6bbcf6a8b935f93575a52d5d5509ac94df130161..4bc4a0502203c41538702d22c19e2f3fc9caea26 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 1637d454cde282e02789bb3a5ae53458193c08e8..0000000000000000000000000000000000000000 --- 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 ddd0f07e78771883c58a5d86e12dc4e3bafc4479..12adfd31b2629800dca5bc4db829173784b90264 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 f06ecb8dcdf0d7682223ae92deb96b5cfe530696..18c4e4fbf90718c6ebdef69c96053fa054bf09fd 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 1ac2e382cbaf7309b40ffbee3c2b47da1d83ca38..90df2b9e9e74cdc0f3189d096c009b31aba077a8 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 18155d5366dc3d6f5778fba8f6193d09143c2f68..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..266329489bc477b806aa4ae876a0ca2771a59596 --- /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 37592dd03f23a930f234c96da18e373a8237b311..0000000000000000000000000000000000000000 --- 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 d38b8acab43c87957d3b705824934a3f2cfd4444..cca109bdf6ba5fa9f5dd85c9862981b8c4b5d816 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; }