Skip to content
Snippets Groups Projects
Commit a3e0a046 authored by René Schöne's avatar René Schöne
Browse files

More polishing.

- Better printing
- Better name analysis
parent 937cb5b8
No related branches found
No related tags found
No related merge requests found
aspect Analysis { aspect Analysis {
syn Set<State> State.reachableWithin(int n) {
if (n == 0) {
return new HashSet<>();
}
Set<State> result = new HashSet<>();
for (State succ : successors()) {
result.add(succ);
result.addAll(succ.reachableWithin(n - 1));
}
return result;
}
syn Set<State> State.reachable() circular [new HashSet<State>()] { syn Set<State> State.reachable() circular [new HashSet<State>()] {
Set<State> result = new HashSet<>(); Set<State> result = new HashSet<>();
result.addAll(successors()); result.addAll(successors());
...@@ -22,34 +10,22 @@ aspect Analysis { ...@@ -22,34 +10,22 @@ aspect Analysis {
public void StateMachine.printSomeAnalysis() { public void StateMachine.printSomeAnalysis() {
Set<Set<State>> sccs = this.SCC(); Set<Set<State>> sccs = this.SCC();
System.out.println("SCCs found:"); System.out.print("SCCs found: ");
for (Set<State> scc : sccs) { for (Set<State> scc : sccs) {
System.out.println(scc); System.out.print(scc + " ");
} }
System.out.println();
for (State s : this.states()) { for (State s : this.states()) {
System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable()); System.out.println(s + ": successors() = " + s.successors() + ", reachable() = " + s.reachable());
} }
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();
}
for (State finalState : this.getFinalList()) { for (State finalState : this.getFinalList()) {
System.out.println("initial state "+ this.getInitial() + " can reach " + finalState + " = " + System.out.println("initial state "+ this.getInitial() + " to " + finalState + " in " +
this.getInitial().reachableWithin(this.states().size()).contains(finalState)); this.getInitial().minDistTo(finalState) + " step(s)");
} }
} }
// --- new ---
syn int State.minDistTo(State other) circular [-1] { syn int State.minDistTo(State other) circular [-1] {
if (this == other) { if (this == other) {
return 0; return 0;
......
aspect NameAnalysis { aspect NameAnalysis {
syn Map<String, State> StateMachine.stateMap() { syn State StateMachine.resolveState(String id) {
Map<String, State> map = new HashMap<>();
for (State s : states()) { for (State s : states()) {
map.put(s.getLabel(), s); if (s.getLabel().equals(id)) {
return s;
}
} }
return map; return null;
} }
syn Map<String, Transition> StateMachine.transitionMap() { syn Transition StateMachine.resolveTransition(String id) {
Map<String, Transition> map = new HashMap<>();
for (Transition t : transitions()) { for (Transition t : transitions()) {
map.put(t.getLabel(), t); if (t.getLabel().equals(id)) {
return t;
}
} }
return map; return null;
} }
refine RefResolverStubs eq ASTNode.globallyResolveStateByToken(String id) { eq StateMachine.globallyResolveStateByToken(String id) = resolveState(id);
return root().stateMap().get(id); eq Element.globallyResolveStateByToken(String id) = containingStateMachine().resolveState(id);
}
refine RefResolverStubs eq ASTNode.globallyResolveTransitionByToken(String id) { eq StateMachine.globallyResolveTransitionByToken(String id) = resolveTransition(id);
return root().transitionMap().get(id); eq Element.globallyResolveTransitionByToken(String id) = containingStateMachine().resolveTransition(id);
}
} }
...@@ -37,12 +37,11 @@ aspect Navigation { ...@@ -37,12 +37,11 @@ aspect Navigation {
return transitions; return transitions;
} }
syn StateMachine ASTNode.root(); inh StateMachine Element.containingStateMachine();
eq StateMachine.root() = this; eq StateMachine.getElement().containingStateMachine() = this;
eq ASTNode.root() = getParent().root();
syn boolean State.isInitial() = root().getInitial().equals(this); syn boolean State.isInitial() = containingStateMachine().getInitial().equals(this);
syn boolean State.isFinal() = root().getFinalList().contains(this); syn boolean State.isFinal() = containingStateMachine().getFinalList().contains(this);
syn Collection<State> State.successors() = getOutgoingList().stream().map(Transition::getTo).collect(Collectors.toList()); syn Collection<State> State.successors() = getOutgoingList().stream().map(Transition::getTo).collect(Collectors.toList());
} }
...@@ -7,62 +7,89 @@ import de.tudresden.inf.st.statemachine.jastadd.model.Transition; ...@@ -7,62 +7,89 @@ import de.tudresden.inf.st.statemachine.jastadd.model.Transition;
import java.io.IOException; import java.io.IOException;
import java.nio.file.Paths; import java.nio.file.Paths;
import java.util.Set;
public class Main { public class Main {
@SuppressWarnings("WeakerAccess") @SuppressWarnings("WeakerAccess")
public static Object DrAST_root_node; public static Object DrAST_root_node;
public static void main(String[] args) { public static void main(String[] args) throws IOException, Parser.Exception {
StateMachine stateMachine;
if (args.length == 0) { if (args.length == 0) {
// manual construction of a simple statemachine stateMachine = createExample();
// (S) -- 1 --> (B) -- 3 --> (E)
// ^ |
// \ /
// `---- 2 ----*
StateMachine stateMachine = new StateMachine();
State start = new State();
start.setLabel("S");
State stateB = new State();
stateB.setLabel("B");
State end = new State();
end.setLabel("E");
Transition t1 = new Transition();
t1.setLabel("1");
Transition t2 = new Transition();
t2.setLabel("2");
Transition t3 = new Transition();
t3.setLabel("3");
t1.setFrom(start);
t1.setTo(stateB);
t2.setFrom(stateB);
t2.setTo(start);
t3.setFrom(stateB);
t3.setTo(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);
System.out.println(stateMachine.prettyPrint());
stateMachine.printSomeAnalysis();
DrAST_root_node = stateMachine;
} else { } else {
// load the file given as first argument // load the file given as first argument
try { stateMachine = ParserUtils.load(Paths.get(args[0]));
StateMachine stateMachine = ParserUtils.load(Paths.get(args[0])); }
stateMachine.treeResolveAll(); printHeading("Initial statemachine");
stateMachine.printSomeAnalysis(); System.out.println(stateMachine.prettyPrint());
System.out.println("> toDotGraph():");
System.out.println(stateMachine.toDot()); stateMachine.printSomeAnalysis();
DrAST_root_node = stateMachine;
} catch (IOException | Parser.Exception e) { Set<Transition> epsilons = stateMachine.epsilonTransitions();
e.printStackTrace();
} for (Transition eps : epsilons) {
printHeading("Removing epsilon transition " + eps.prettyPrint().trim());
System.out.println("Minimal distances before:");
initialToFinalDistances(stateMachine);
stateMachine.removeEpsilonTransition(eps);
System.out.println("Minimal distances after:");
initialToFinalDistances(stateMachine);
printHeading("StateMachine after");
System.out.println(stateMachine.prettyPrint());
}
printHeading("DotGraph");
System.out.println(stateMachine.toDot());
DrAST_root_node = stateMachine;
}
private static void printHeading(String s) {
System.out.println();
System.out.println("========================================");
System.out.println("== " + s);
System.out.println("========================================");
}
private static StateMachine createExample() {
// manual construction of a simple statemachine
// (S) -- e --> (B) -- 1 --> (E)
// ^ |
// \ /
// `---- 2 ----*
StateMachine stateMachine = new StateMachine();
State start = new State();
start.setLabel("S");
State stateB = new State();
stateB.setLabel("B");
State end = new State();
end.setLabel("E");
Transition eps = new Transition();
Transition t2 = new Transition();
t2.setLabel("2");
Transition t1 = new Transition();
t1.setLabel("1");
eps.setFrom(start);
eps.setTo(stateB);
t2.setFrom(stateB);
t2.setTo(start);
t1.setFrom(stateB);
t1.setTo(end);
stateMachine.addElement(start);
stateMachine.addElement(stateB);
stateMachine.addElement(end);
stateMachine.addElement(eps);
stateMachine.addElement(t2);
stateMachine.addElement(t1);
stateMachine.setInitial(start);
stateMachine.addFinal(end);
return stateMachine;
}
private static void initialToFinalDistances(StateMachine stateMachine) {
for (State finalState : stateMachine.getFinalList()) {
System.out.println("initial state "+ stateMachine.getInitial() + " to " + finalState + " in " +
stateMachine.getInitial().minDistTo(finalState) + " step(s)");
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment