diff --git a/statemachine/build.gradle b/statemachine/build.gradle index f0aad7522477fa80eeb1e55b2f2272b900fefa5d..cf7835e9d8ae4b2cbd0e890da1dc21ab06862986 100644 --- a/statemachine/build.gradle +++ b/statemachine/build.gradle @@ -46,9 +46,6 @@ dependencies { run { mainClassName = 'de.tudresden.inf.st.statemachine.Main' standardInput = System.in - if (project.hasProperty("appArgs")) { - args Eval.me(appArgs) - } } buildscript { diff --git a/statemachine/src/main/jastadd/Analysis.jrag b/statemachine/src/main/jastadd/Analysis.jrag index 427e0b137e9a55d91e59852c7e07a3acb4201e42..872fa7cd18626b741bca378833ef326a58df056d 100644 --- a/statemachine/src/main/jastadd/Analysis.jrag +++ b/statemachine/src/main/jastadd/Analysis.jrag @@ -1,32 +1,42 @@ aspect Analysis { - syn Map<String, State> StateMachine.stateMap() { - Map<String, State> map = new HashMap<>(); - for (State s : states()) { - map.put(s.getLabel(), s); + syn Set<State> State.reachableWithin(int n) { //circular [new HashSet<>()] + if (n == 0) { + return new HashSet<>(); } - return map; + Set<State> result = new HashSet<>(); + for (State succ : successors()) { + result.add(succ); + result.addAll(succ.reachableWithin(n - 1)); + } + return result; } - syn Map<String, Transition> StateMachine.transitionMap() { - Map<String, Transition> map = new HashMap<>(); - for (Transition t : transitions()) { - map.put(t.getLabel(), t); + public void StateMachine.printSomeAnalysis() { + // analysis + Set<Set<State>> sccs = this.SCC(); + System.out.println("SCCs found:"); + for (Set<State> scc : sccs) { + System.out.println(scc); } - return map; - } - syn StateMachine ASTNode.root(); - eq StateMachine.root() = this; - eq ASTNode.root() = getParent().root(); + for (State s : this.states()) { + System.out.println(s + ".successors() = " + s.successors()); + } - refine RefResolverStubs eq ASTNode.globallyResolveStateByToken(String id) { - return root().stateMap().get(id); - } + Set<State> current; + int lastSize = 0; + for (int i = 1; i < this.states().size() + 1; i++) { + current = this.getInitial().reachableWithin(i); + if (current.size() == lastSize) { + break; + } + System.out.println(this.getInitial() + ".reachableWithin(" + i + ") = " + current); + lastSize = current.size(); + } - refine RefResolverStubs eq ASTNode.globallyResolveTransitionByToken(String id) { - return root().transitionMap().get(id); + for (State finalState : this.getFinalList()) { + System.out.println("initial state "+ this.getInitial() + " can reach " + finalState + " = " + + this.getInitial().reachableWithin(this.states().size()).contains(finalState)); + } } - - syn boolean State.isInitial() = root().getInitial().equals(this); - syn boolean State.isFinal() = root().getFinalList().contains(this); } diff --git a/statemachine/src/main/jastadd/NameAnalysis.jrag b/statemachine/src/main/jastadd/NameAnalysis.jrag new file mode 100644 index 0000000000000000000000000000000000000000..41cc7f687924158b825faaf6823b611a2cf9822b --- /dev/null +++ b/statemachine/src/main/jastadd/NameAnalysis.jrag @@ -0,0 +1,25 @@ +aspect NameAnalysis { + syn Map<String, State> StateMachine.stateMap() { + Map<String, State> map = new HashMap<>(); + for (State s : states()) { + map.put(s.getLabel(), s); + } + return map; + } + + syn Map<String, Transition> StateMachine.transitionMap() { + Map<String, Transition> map = new HashMap<>(); + for (Transition t : transitions()) { + map.put(t.getLabel(), t); + } + return map; + } + + refine RefResolverStubs eq ASTNode.globallyResolveStateByToken(String id) { + return root().stateMap().get(id); + } + + refine RefResolverStubs eq ASTNode.globallyResolveTransitionByToken(String id) { + return root().transitionMap().get(id); + } +} diff --git a/statemachine/src/main/jastadd/Navigation.jrag b/statemachine/src/main/jastadd/Navigation.jrag index c6b1500b2b8eb2d2c84c0a4cef19447807f4d205..0ccd14a71897c8831bc70a881cacfd0b7c5dd8a5 100644 --- a/statemachine/src/main/jastadd/Navigation.jrag +++ b/statemachine/src/main/jastadd/Navigation.jrag @@ -31,4 +31,13 @@ aspect Navigation { } return transitions; } + + syn StateMachine ASTNode.root(); + eq StateMachine.root() = this; + eq ASTNode.root() = getParent().root(); + + syn boolean State.isInitial() = root().getInitial().equals(this); + syn boolean State.isFinal() = root().getFinalList().contains(this); + + syn Collection<State> State.successors() = getOutgoingList().stream().map(Transition::getTo).collect(Collectors.toList()); } diff --git a/statemachine/src/main/jastadd/SMtoDotG.jrag b/statemachine/src/main/jastadd/SMtoDotG.jrag new file mode 100644 index 0000000000000000000000000000000000000000..18155d5366dc3d6f5778fba8f6193d09143c2f68 --- /dev/null +++ b/statemachine/src/main/jastadd/SMtoDotG.jrag @@ -0,0 +1,18 @@ +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/src/main/java/de/tudresden/inf/st/statemachine/Main.java b/statemachine/src/main/java/de/tudresden/inf/st/statemachine/Main.java index c10cff5f340983827a57aac27c7894aea33ee578..ea757e857e6616c29c30471d347bd3e0bae6f81b 100644 --- a/statemachine/src/main/java/de/tudresden/inf/st/statemachine/Main.java +++ b/statemachine/src/main/java/de/tudresden/inf/st/statemachine/Main.java @@ -1,6 +1,7 @@ package de.tudresden.inf.st.statemachine; import beaver.Parser; +import de.tudresden.inf.st.statemachine.jastadd.model.DotGraph; 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; @@ -21,7 +22,7 @@ public class Main { // ^ | // \ / // `---- 2 ----* - StateMachine statemachine = new StateMachine(); + StateMachine stateMachine = new StateMachine(); State start = new State(); start.setLabel("S"); State stateB = new State(); @@ -40,24 +41,26 @@ public class Main { t2.setTo(start); t3.setFrom(stateB); t3.setTo(end); - statemachine.addElement(start); - statemachine.addElement(stateB); - statemachine.addElement(end); - statemachine.setInitial(start); - statemachine.addFinal(end); + stateMachine.addElement(start); + stateMachine.addElement(stateB); + stateMachine.addElement(end); + stateMachine.addElement(t1); + stateMachine.addElement(t2); + stateMachine.addElement(t3); + stateMachine.setInitial(start); + stateMachine.addFinal(end); - // reachability analysis - Set<Set<State>> sccs = statemachine.SCC(); - System.out.println("SCCs found:"); - for (Set<State> scc : sccs) { - System.out.println(scc); - } - DrAST_root_node = statemachine; + System.out.println(stateMachine.prettyPrint()); + stateMachine.printSomeAnalysis(); + DrAST_root_node = stateMachine; } else { // load the file given as first argument try { StateMachine stateMachine = ParserUtils.load(Paths.get(args[0])); stateMachine.treeResolveAll(); + stateMachine.printSomeAnalysis(); + System.out.println("> toDotGraph():"); + System.out.println(stateMachine.toDot()); DrAST_root_node = stateMachine; } catch (IOException | Parser.Exception e) { e.printStackTrace(); diff --git a/statemachine/src/test/resources/telephone.sm b/statemachine/src/test/resources/telephone.sm new file mode 100644 index 0000000000000000000000000000000000000000..655e5bb364d93430b97cc7dfd5e28a338436cdfe --- /dev/null +++ b/statemachine/src/test/resources/telephone.sm @@ -0,0 +1,25 @@ +initial state start; +state onHook; +state dialing; +state ringing; +state waitingForConnection; +state communicating; +state onHold; +final state end; + +trans start -> onHook : start ; +trans onHook -> dialing : startDialing ; +trans dialing -> onHook : hangUp ; +trans onHook -> ringing : incomingCall ; +trans ringing -> onHook : otherPartyHangUp ; +trans dialing -> waitingForConnection : completeNumber ; +trans waitingForConnection -> onHook : hangUp ; +trans waitingForConnection -> onHook : timeOut ; +trans waitingForConnection -> communicating : otherPartyPickUp ; +trans ringing -> communicating : pickUp ; +trans communicating -> onHook : hangUp ; +trans communicating -> onHold : putOnHold ; +trans onHold -> communicating : takeOffHold ; +trans communicating -> end : otherPartyHangUp ; +trans onHold -> end : otherPartyHangUp ; +trans onHold -> end : hangUp ;