getEndNodes() {
+ return this.endNodes;
+ }
+ }
+
+ /**
+ * This method builds a {@link SubStateMachine} equivalent to the given {@link Order}.
+ *
+ * It is called recursively For a collection of start nodes, which must already be added to
+ * the {@link StateMachineGraph} result.
+ *
+ * @param order The CrySL {@link Order} Expression to build the {@link SubStateMachine} for.
+ * @param startNodes Set of nodes used as the startNodes of this {@link SubStateMachine}.
+ * @return the {@link SubStateMachine} representing this {@link Order} Expression
+ *
Having a look at the Crysl Xtext definition for the Order section, we have -----------
+ *
+ * Sequence returns Order:
+ * Alternative ({Order.left=current} op=SequenceOperator right=Alternative)*
+ * ;
+ *
+ * enum SequenceOperator returns OrderOperator:
+ * SEQUENCE = ','
+ * ;
+ *
+ *
+ * Alternative returns Order:
+ * Cardinality ({Order.left=current} op=AlternativeOperator right=Cardinality)*
+ * ;
+ *
+ *
+ * enum AlternativeOperator returns OrderOperator:
+ * ALTERNATIVE = '|'
+ * ;
+ *
+ *
+ * Cardinality returns Order:
+ * Primary ({Order.left=current} op = CardinalityOperator)?
+ * ;
+ *
+ *
+ * enum CardinalityOperator returns OrderOperator:
+ * ZERO_OR_MORE = '*' | ONE_OR_MORE = '+' | ZERO_OR_ONE = '?'
+ * ;
+ *
+ *
+ * Primary returns Order:
+ * {Primary} event = [Event]
+ * | '(' Order ')'
+ * ;
+ *
+ * -----------
+ *
Based on this definition, the method will build the StateMachine from the Order
+ * section.
+ *
This is done by recursively building a sub-StateMachine and connecting it with given
+ * start Nodes and returned end Nodes according to the specific OrderOperator.
+ *
Therefore, consider the following cases
+ *
1. Order instanceof Primary: In this case, we create a new Node and add a transition
+ * for the Event from each start Node to the newly created Node. Finally, we return a
+ * SubStateMachine where the newly created node is the start and end Node.
+ *
2. OrderOperator == SEQUENCE: The left-side should occur before the right-side. We
+ * therefore recursively build the sub-StateMachine of the left-side with the given start
+ * Nodes saving the returned end Nodes. We then build the sub-StateMachine of the right-side
+ * giving it the left-side's end Nodes as start Nodes. Finally, we return the startNodes of
+ * the left-side's start Nodes as our start Nodes and the end Nodes of the right-side's
+ * sub-StateMachine as our end Nodes.
+ *
3. OrderOperator == ALTERNATIVE: Either the left-side or the right-side should occur.
+ * We therefore build both sub-StateMachines with our start Nodes as start Nodes. Finally,
+ * we return the aggregate of both start Nodes as our startNodes and the aggregates of both
+ * end Nodes as our end Nodes.
+ *
4. OrderOperator == ZERO_OR_ONE: The Event can occur or be skipped. We therefore build
+ * the sub-StateMachine (only the left-side is present) with our start Nodes as start Nodes.
+ * Finally, we return the returned start Nodes as our start Nodes and the returned Nodes end
+ * Nodes (event occurs) and our start nodes (event skipped) as end Nodes.
+ *
5. OrderOperator == ONE_OR_MORE: The Event can occur once or multiple times. We
+ * therefore build the sub-StateMachine (only the left-side is present) with our start Nodes
+ * as start Nodes and save the returned end Nodes. We then duplicate the transitions from
+ * each given start Node to the start node of the Sub-StateMachine, but not with the given
+ * start Node as origin, but each end Node of the Sub-StateMachine, this creates the desired
+ * loop. Finally, we return the returned start and end Nodes.
+ *
5. OrderOperator == ZERO_OR_MORE: This can be seen as (Order)*?. We therefore proceed
+ * as in ONE_OR_MORE but additionally return the given start Nodes as end Nodes as well as
+ * in ZERO_OR_ONE.
+ */
+ private SubStateMachine buildSubSMG(final Order order, final Collection startNodes) {
+
+ if (order == null) {
+ // This is the case if the ORDER section was omitted.
+ // It implies, that any method may be called in any sequence.
+ // We therefore create a Node and a transition from all startNodes
+ // to this node and a loop from the node to itself.
+ StateNode node = this.result.createNewNode();
+ node.setAccepting(true);
+ Collection label = new HashSet<>(retrieveAllMethodsFromEvents());
+
+ for (StateNode startNode : startNodes) {
+ this.result.createNewEdge(label, startNode, node);
+ }
+
+ this.result.createNewEdge(label, node, node);
+ return new SubStateMachine(Collections.singleton(node), startNodes);
+ }
+
+ if (order instanceof Primary) {
+ Event event = ((Primary) order).getEvent();
+ StateNode node = this.result.createNewNode();
+ Collection label = CrySLReaderUtils.resolveEventToCryslMethods(event);
+
+ for (StateNode startNode : startNodes) {
+ this.result.createNewEdge(label, startNode, node);
+ }
+
+ return new SubStateMachine(node, node);
+ }
+
+ Collection end = new HashSet<>();
+ Collection start = new HashSet<>();
+
+ final SubStateMachine left;
+ final SubStateMachine right;
+
+ switch (order.getOp()) {
+ case SEQUENCE:
+ left = buildSubSMG(order.getLeft(), startNodes);
+ right = buildSubSMG(order.getRight(), left.getEndNodes());
+ start.addAll(left.getStartNodes());
+ end.addAll(right.getEndNodes());
+
+ for (StateNode node : startNodes) {
+ if (left.getEndNodes().contains(node)) {
+ start.addAll(right.getStartNodes());
+ }
+ }
+
+ break;
+ case ALTERNATIVE:
+ left = buildSubSMG(order.getLeft(), startNodes);
+ right = buildSubSMG(order.getRight(), startNodes);
+ start.addAll(left.getStartNodes());
+ start.addAll(right.getStartNodes());
+ end.addAll(left.getEndNodes());
+ end.addAll(right.getEndNodes());
+ // TODO For some reason, this part removes loops in accepting states
+ /* reduce all end nodes without outgoing edges to one end node
+ * Set endNodesWithOutgoingEdges =
+ * this.result.getEdges().parallelStream()
+ * .map(edge -> edge.from()).filter(node ->
+ * end.contains(node)).collect(Collectors.toSet());
+ * if (endNodesWithOutgoingEdges.size() < end.size() - 1) {
+ * end.removeAll(endNodesWithOutgoingEdges);
+ * StateNode aggrNode = this.result.aggregateNodesToOneNode(end,
+ * end.iterator().next());
+ * end.clear();
+ * end.add(aggrNode);
+ * end.addAll(endNodesWithOutgoingEdges);
+ * }
+ */
+ break;
+ case ONE_OR_MORE:
+ case ZERO_OR_MORE:
+ case ZERO_OR_ONE:
+ left = buildSubSMG(order.getLeft(), startNodes);
+ start.addAll(left.getStartNodes());
+ end.addAll(left.getEndNodes());
+ if (order.getOp() == OrderOperator.ZERO_OR_MORE
+ || order.getOp() == OrderOperator.ONE_OR_MORE) {
+ startNodes.stream()
+ .map(this.result::getAllOutgoingEdges)
+ .flatMap(Collection::stream)
+ .filter(edge -> left.getStartNodes().contains(edge.getRight()))
+ .forEach(
+ edge ->
+ left.getEndNodes()
+ .forEach(
+ endNode ->
+ this.result.createNewEdge(
+ edge.getLabel(),
+ endNode,
+ edge.getRight())));
+ }
+ if (order.getOp() == OrderOperator.ZERO_OR_MORE
+ || order.getOp() == OrderOperator.ZERO_OR_ONE) {
+ end.addAll(startNodes);
+ }
+ break;
+ }
+ return new SubStateMachine(start, end);
+ }
+
+ private Collection retrieveAllMethodsFromEvents() {
+ if (this.allMethods.isEmpty())
+ this.allMethods.addAll(CrySLReaderUtils.resolveEventsToCryslMethods(this.events));
+ return this.allMethods;
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLArithmeticConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLArithmeticConstraint.java
new file mode 100644
index 0000000..ab27d82
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLArithmeticConstraint.java
@@ -0,0 +1,87 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class CrySLArithmeticConstraint extends CrySLLiteral {
+
+ public enum ArithOp {
+ p,
+ n,
+ m
+ }
+
+ /* p = +
+ * n = -
+ * m = %
+ */
+
+ private final ArithOp operator;
+ private final ICrySLPredicateParameter left;
+ private final ICrySLPredicateParameter right;
+
+ public CrySLArithmeticConstraint(
+ ICrySLPredicateParameter l, ICrySLPredicateParameter r, ArithOp op) {
+ left = l;
+ right = r;
+ operator = op;
+ }
+
+ /**
+ * @return the operator
+ */
+ public ArithOp getOperator() {
+ return operator;
+ }
+
+ /**
+ * @return the left
+ */
+ public ICrySLPredicateParameter getLeft() {
+ return left;
+ }
+
+ /**
+ * @return the right
+ */
+ public ICrySLPredicateParameter getRight() {
+ return right;
+ }
+
+ public String toString() {
+ return left
+ + " "
+ + (operator.equals(ArithOp.p) ? "+" : (operator.equals(ArithOp.m) ? "%" : "-"))
+ + " "
+ + right;
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ List varNames = new ArrayList<>();
+ String name = left.getName();
+ if (!isIntOrBoolean(name)) {
+ varNames.add(name);
+ }
+
+ name = right.getName();
+ if (!isIntOrBoolean(name)) {
+ varNames.add(name);
+ }
+ return varNames;
+ }
+
+ private boolean isIntOrBoolean(String name) {
+ try {
+ Integer.parseInt(name);
+ return true;
+ } catch (NumberFormatException ex) {
+ return name.equalsIgnoreCase("false") || name.equalsIgnoreCase("true");
+ }
+ }
+
+ @Override
+ public String getName() {
+ return toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLComparisonConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLComparisonConstraint.java
new file mode 100644
index 0000000..9b550b8
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLComparisonConstraint.java
@@ -0,0 +1,80 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.List;
+
+public class CrySLComparisonConstraint extends CrySLLiteral {
+
+ public enum CompOp {
+ l,
+ g,
+ le,
+ ge,
+ eq,
+ neq
+ }
+
+ private final CompOp operator;
+ private final CrySLArithmeticConstraint left;
+ private final CrySLArithmeticConstraint right;
+
+ public CrySLComparisonConstraint(
+ CrySLArithmeticConstraint l, CrySLArithmeticConstraint r, CompOp op) {
+ left = l;
+ right = r;
+ operator = op;
+ }
+
+ public String toString() {
+ return left + " " + getOperatorString() + " " + right;
+ }
+
+ private String getOperatorString() {
+ switch (operator) {
+ case l:
+ return "<";
+ case le:
+ return "<=";
+ case g:
+ return ">";
+ case ge:
+ return ">=";
+ case neq:
+ return "!=";
+ default:
+ return "=";
+ }
+ }
+
+ /**
+ * @return the operator
+ */
+ public CompOp getOperator() {
+ return operator;
+ }
+
+ /**
+ * @return the left
+ */
+ public CrySLArithmeticConstraint getLeft() {
+ return left;
+ }
+
+ /**
+ * @return the right
+ */
+ public CrySLArithmeticConstraint getRight() {
+ return right;
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ List varNames = left.getInvolvedVarNames();
+ varNames.addAll(right.getInvolvedVarNames());
+ return varNames;
+ }
+
+ @Override
+ public String getName() {
+ return toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLCondPredicate.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLCondPredicate.java
new file mode 100644
index 0000000..d49dfdc
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLCondPredicate.java
@@ -0,0 +1,52 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+import java.util.List;
+
+public class CrySLCondPredicate extends CrySLPredicate {
+
+ private final Collection conditionalNodes;
+
+ public CrySLCondPredicate(
+ ICrySLPredicateParameter baseObj,
+ String name,
+ List parameters,
+ Boolean negated,
+ Collection nodes) {
+ this(baseObj, name, parameters, negated, nodes, null);
+ }
+
+ public CrySLCondPredicate(
+ ICrySLPredicateParameter baseObj,
+ String name,
+ List parameters,
+ Boolean negated,
+ Collection nodes,
+ ISLConstraint constraint) {
+ super(baseObj, name, parameters, negated, constraint);
+ this.conditionalNodes = nodes;
+ }
+
+ /**
+ * @return the conditionalMethods
+ */
+ public Collection getConditionalMethods() {
+ return conditionalNodes;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (!super.equals(obj)) return false;
+
+ if (!(obj instanceof CrySLCondPredicate)) return false;
+
+ CrySLCondPredicate other = (CrySLCondPredicate) obj;
+ if (!getConditionalMethods().equals(other.getConditionalMethods())) return false;
+
+ return true;
+ }
+
+ public String toString() {
+ return super.toString() + " after " + conditionalNodes;
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLConstraint.java
new file mode 100644
index 0000000..e950257
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLConstraint.java
@@ -0,0 +1,64 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.List;
+
+public class CrySLConstraint implements ISLConstraint {
+
+ public enum LogOps {
+ and,
+ or,
+ implies,
+ eq
+ }
+
+ private final LogOps operator;
+ private final ISLConstraint left;
+ private final ISLConstraint right;
+
+ public CrySLConstraint(ISLConstraint l, ISLConstraint r, LogOps op) {
+ left = l;
+ right = r;
+ operator = op;
+ }
+
+ /**
+ * @return the operator return operator;
+ */
+ public LogOps getOperator() {
+ return operator;
+ }
+
+ /**
+ * @return the left
+ */
+ public ISLConstraint getLeft() {
+ return left;
+ }
+
+ /**
+ * @return the right
+ */
+ public ISLConstraint getRight() {
+ return right;
+ }
+
+ public String toString() {
+ StringBuilder constraintSB = new StringBuilder();
+ constraintSB.append(left.toString());
+ constraintSB.append(operator);
+ constraintSB.append(right.toString());
+ return constraintSB.toString();
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ List varNames = left.getInvolvedVarNames();
+ varNames.addAll(right.getInvolvedVarNames());
+ return varNames;
+ }
+
+ @Override
+ public String getName() {
+ return toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLException.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLException.java
new file mode 100644
index 0000000..29fdd28
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLException.java
@@ -0,0 +1,28 @@
+package de.darmstadt.tu.crossing.rule;
+
+/** Helper Class to store an {@link Exception} as a String. */
+public class CrySLException {
+
+ private final String exception;
+
+ /**
+ * Construct a {@link CrySLException} from the fully qualified classname of the {@link
+ * Exception} to store.
+ *
+ * @param exception the exception's name
+ */
+ public CrySLException(String exception) {
+ this.exception = exception;
+ }
+
+ /**
+ * @return The fully qualified classname of the stored {@link Exception}.
+ */
+ public String getException() {
+ return exception;
+ }
+
+ public String toString() {
+ return String.format("%s(%s)", this.getClass().getName(), this.exception);
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLExceptionConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLExceptionConstraint.java
new file mode 100644
index 0000000..d1114ca
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLExceptionConstraint.java
@@ -0,0 +1,61 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collections;
+import java.util.List;
+
+/**
+ * Constraint expressing, that a {@link CrySLMethod} throws an {@link CrySLException}, that must be
+ * caught.
+ */
+public class CrySLExceptionConstraint implements ISLConstraint {
+
+ /** The Method throwing the Exception. */
+ private final CrySLMethod method;
+
+ /** The Exception thrown by the Method. */
+ private final CrySLException exception;
+
+ /**
+ * Construct the {@link CrySLExceptionConstraint} given the method and the exception thrown
+ * thereby.
+ *
+ * @param method Method that throws the Exception.
+ * @param exception Exception that thrown by the Method.
+ */
+ public CrySLExceptionConstraint(CrySLMethod method, CrySLException exception) {
+ this.method = method;
+ this.exception = exception;
+ }
+
+ /**
+ * Returns the Method throwing the Exception.
+ *
+ * @return The Method throwing the Exception.
+ */
+ public CrySLMethod getMethod() {
+ return method;
+ }
+
+ /**
+ * Returns the Exception thrown by the Exception.
+ *
+ * @return The Exception thrown by the Exception.
+ */
+ public CrySLException getException() {
+ return exception;
+ }
+
+ public String toString() {
+ return String.format("%s(%s, %s)", this.getClass().getName(), getMethod(), getException());
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ return Collections.emptyList();
+ }
+
+ @Override
+ public String getName() {
+ return toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLForbiddenMethod.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLForbiddenMethod.java
new file mode 100644
index 0000000..4ed8103
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLForbiddenMethod.java
@@ -0,0 +1,55 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+
+public class CrySLForbiddenMethod {
+
+ private final CrySLMethod method;
+ private final Collection alternatives;
+
+ public CrySLForbiddenMethod(CrySLMethod method, Collection alternatives) {
+ this.method = method;
+ this.alternatives = alternatives;
+ }
+
+ public CrySLMethod getMethod() {
+ return method;
+ }
+
+ public Collection getAlternatives() {
+ return alternatives;
+ }
+
+ @Override
+ public String toString() {
+ final StringBuilder forbiddenMethod = new StringBuilder();
+ forbiddenMethod.append(method.toString());
+ if (!alternatives.isEmpty()) {
+ forbiddenMethod.append(" Alternatives: ");
+ }
+
+ for (CrySLMethod meth : alternatives) {
+ forbiddenMethod.append(meth.toString());
+ }
+
+ return forbiddenMethod.toString();
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) {
+ return true;
+ }
+
+ if (!(obj instanceof CrySLForbiddenMethod)) {
+ return false;
+ }
+
+ CrySLForbiddenMethod other = (CrySLForbiddenMethod) obj;
+ if (!method.equals(other.getMethod())) {
+ return false;
+ }
+
+ return alternatives.equals(other.getAlternatives());
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLLiteral.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLLiteral.java
new file mode 100644
index 0000000..4f328d8
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLLiteral.java
@@ -0,0 +1,6 @@
+package de.darmstadt.tu.crossing.rule;
+
+public abstract class CrySLLiteral implements ISLConstraint {
+
+ protected CrySLLiteral() {}
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLMethod.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLMethod.java
new file mode 100644
index 0000000..7efc085
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLMethod.java
@@ -0,0 +1,121 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.stream.Collectors;
+
+public class CrySLMethod implements ICrySLPredicateParameter {
+
+ public static final String VOID = "void";
+ public static final String ANY_TYPE = "AnyType";
+ public static final String NO_NAME = "_";
+
+ private final String methodName;
+ private final String declaringClassName;
+ private final Entry retObject;
+
+ /**
+ * List of Parameters, where a Parameter is an {@link Entry} of Name and Type, both as {@link
+ * String}.
+ */
+ private final List> parameters;
+
+ public CrySLMethod(
+ String methodName,
+ String declaringClassName,
+ List> parameters,
+ Entry retObject) {
+ this.methodName = methodName;
+ this.declaringClassName = declaringClassName;
+ this.parameters = parameters;
+ this.retObject = retObject;
+ }
+
+ /**
+ * @return the FQ methodName
+ */
+ public String getMethodName() {
+ return methodName;
+ }
+
+ /**
+ * @return the short methodName
+ */
+ public String getShortMethodName() {
+ return methodName.substring(methodName.lastIndexOf(".") + 1);
+ }
+
+ public String getDeclaringClassName() {
+ return declaringClassName;
+ }
+
+ /**
+ * @return the parameters
+ */
+ public List> getParameters() {
+ return parameters;
+ }
+
+ public Entry getRetObject() {
+ return retObject;
+ }
+
+ public String toString() {
+ return getName();
+ }
+
+ public String getSignature() {
+ return getMethodName()
+ + "("
+ + parameters.stream()
+ .map(param -> String.format("%s", param.getValue()))
+ .collect(Collectors.joining(", "))
+ + ")";
+ }
+
+ @Override
+ public String getName() {
+ StringBuilder stmntBuilder = new StringBuilder();
+ String returnValue = retObject.getKey();
+ if (!"_".equals(returnValue)) {
+ stmntBuilder.append(returnValue);
+ stmntBuilder.append(" = ");
+ }
+
+ stmntBuilder.append(this.methodName);
+ stmntBuilder.append("(");
+
+ stmntBuilder.append(
+ parameters.stream()
+ .map(param -> String.format("%s %s", param.getValue(), param.getKey()))
+ .collect(Collectors.joining(", ")));
+
+ stmntBuilder.append(");");
+ return stmntBuilder.toString();
+ }
+
+ @Override
+ public int hashCode() {
+ final int prime = 31;
+ int result = 1;
+ result = prime * result + ((methodName == null) ? 0 : methodName.hashCode());
+ result = prime * result + ((parameters == null) ? 0 : parameters.hashCode());
+ return result;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) {
+ return true;
+ }
+ if (obj == null) {
+ return false;
+ }
+ if (!(obj instanceof CrySLMethod)) {
+ return false;
+ }
+ CrySLMethod other = (CrySLMethod) obj;
+ return this.getMethodName().equals(other.getMethodName())
+ && parameters.equals(other.parameters);
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLObject.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLObject.java
new file mode 100644
index 0000000..dff929d
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLObject.java
@@ -0,0 +1,64 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Arrays;
+
+public class CrySLObject implements ICrySLPredicateParameter {
+
+ private final String varName;
+ private final String javaType;
+ private final CrySLSplitter splitter;
+
+ public CrySLObject(String name, String type) {
+ this(name, type, null);
+ }
+
+ public CrySLObject(String name, String type, CrySLSplitter part) {
+ varName = name;
+ javaType = type;
+ splitter = part;
+ }
+
+ /**
+ * @return the varName
+ */
+ public String getVarName() {
+ return varName;
+ }
+
+ /**
+ * @return the splitter
+ */
+ public CrySLSplitter getSplitter() {
+ return splitter;
+ }
+
+ @Override
+ public boolean equals(Object other) {
+ if (other == this) return true;
+ if (other == null) return false;
+ if (!(other instanceof CrySLObject)) return false;
+ CrySLObject object = (CrySLObject) other;
+ return this.getJavaType().equals(object.getJavaType())
+ && this.getName().equals(object.getName())
+ && (this.getSplitter() == null || this.getSplitter().equals(object.getSplitter()));
+ }
+
+ @Override
+ public int hashCode() {
+ return Arrays.hashCode(new Object[] {varName, javaType, splitter});
+ }
+
+ @Override
+ public String toString() {
+ return javaType + " " + varName + ((splitter != null) ? splitter.toString() : "");
+ }
+
+ @Override
+ public String getName() {
+ return varName;
+ }
+
+ public String getJavaType() {
+ return javaType;
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLPredicate.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLPredicate.java
new file mode 100644
index 0000000..f0e7fd7
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLPredicate.java
@@ -0,0 +1,156 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+import java.util.Optional;
+import java.util.stream.Collectors;
+
+public class CrySLPredicate extends CrySLLiteral {
+
+ protected final ICrySLPredicateParameter baseObject;
+ protected final String predName;
+ protected final List parameters;
+ protected final boolean negated;
+ protected final ISLConstraint constraint;
+
+ public CrySLPredicate(
+ ICrySLPredicateParameter baseObject,
+ String name,
+ List parameters,
+ Boolean negated) {
+ this(baseObject, name, parameters, negated, null);
+ }
+
+ public CrySLPredicate(
+ ICrySLPredicateParameter baseObject,
+ String name,
+ List parameters,
+ Boolean negated,
+ ISLConstraint constraint) {
+ this.baseObject = baseObject;
+ this.predName = name;
+ this.parameters = parameters;
+ this.negated = negated;
+ this.constraint = constraint;
+ }
+
+ @Override
+ public int hashCode() {
+ return Arrays.hashCode(new Object[] {predName, parameters.size(), negated});
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) {
+ return true;
+ }
+
+ if (!(obj instanceof CrySLPredicate)) {
+ return false;
+ }
+
+ CrySLPredicate other = (CrySLPredicate) obj;
+ if (baseObject == null) {
+ if (other.getBaseObject() != null) return false;
+ } else if (!baseObject.equals(other.getBaseObject())) {
+ return false;
+ }
+
+ if (predName == null) {
+ if (other.getPredName() != null) return false;
+ } else if (!predName.equals(other.getPredName())) {
+ return false;
+ }
+
+ if (parameters == null) {
+ if (other.getParameters() != null) return false;
+ } else if (parameters.size() != other.getParameters().size()) {
+ return false;
+ }
+
+ return negated == other.isNegated();
+ }
+
+ /**
+ * @return the baseObject
+ */
+ public ICrySLPredicateParameter getBaseObject() {
+ return baseObject;
+ }
+
+ /**
+ * @return the predName
+ */
+ public String getPredName() {
+ return predName;
+ }
+
+ /**
+ * @return the optConstraint
+ */
+ public Optional getConstraint() {
+ return Optional.ofNullable(constraint);
+ }
+
+ /**
+ * @return the parameters
+ */
+ public List getParameters() {
+ return parameters;
+ }
+
+ /**
+ * @return the negated
+ */
+ public Boolean isNegated() {
+ return negated;
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder predSB = new StringBuilder();
+ if (negated) predSB.append("!");
+ predSB.append(predName);
+ predSB.append("(");
+ predSB.append(parameters.stream().map(Object::toString).collect(Collectors.joining(", ")));
+ predSB.append(")");
+
+ return predSB.toString();
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ List varNames = new ArrayList<>();
+ if (Arrays.asList(new String[] {"neverTypeOf", "instanceOf"}).contains(predName)) {
+ varNames.add(parameters.get(0).getName());
+ } else {
+ for (ICrySLPredicateParameter var : parameters) {
+ if (!("_".equals(var.getName())
+ || "this".equals(var.getName())
+ || var instanceof CrySLMethod)) {
+ varNames.add(var.getName());
+ }
+ }
+ }
+ if (getBaseObject() != null) varNames.add(getBaseObject().getName());
+ return varNames;
+ }
+
+ public CrySLPredicate invertNegation() {
+ return new CrySLPredicate(baseObject, predName, parameters, !negated);
+ }
+
+ public CrySLPredicate toNormalCrySLPredicate() {
+ return new CrySLPredicate(baseObject, predName, parameters, negated, constraint);
+ }
+
+ @Override
+ public String getName() {
+ if (parameters.size() == 1) {
+ return parameters.get(0).getName();
+ } else {
+ return "";
+ }
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLRule.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLRule.java
new file mode 100644
index 0000000..9c43463
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLRule.java
@@ -0,0 +1,171 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+import java.util.LinkedList;
+import java.util.Map;
+
+public class CrySLRule {
+
+ private final String className;
+
+ private final Collection> objects;
+
+ private final Collection forbiddenMethods;
+
+ private final Collection events;
+
+ private final StateMachineGraph usagePattern;
+
+ private final Collection constraints;
+
+ private final Collection predicates;
+
+ private final Collection negatedPredicates;
+
+ public CrySLRule(
+ String className,
+ Collection> objects,
+ Collection forbiddenMethods,
+ Collection events,
+ StateMachineGraph usagePattern,
+ Collection constraints,
+ Collection predicates,
+ Collection negatedPredicates) {
+ this.className = className;
+ this.objects = objects;
+ this.forbiddenMethods = forbiddenMethods;
+ this.events = events;
+ this.usagePattern = usagePattern;
+ this.constraints = constraints;
+ this.predicates = predicates;
+ this.negatedPredicates = negatedPredicates;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (obj instanceof CrySLRule) {
+ return ((CrySLRule) obj).getClassName().equals(className);
+ }
+ return false;
+ }
+
+ @Override
+ public int hashCode() {
+ return 31 * className.hashCode();
+ }
+
+ /**
+ * @return the className
+ */
+ public String getClassName() {
+ return className;
+ }
+
+ /**
+ * @return the objects
+ */
+ public Collection> getObjects() {
+ return objects;
+ }
+
+ /**
+ * @return the forbiddenMethods
+ */
+ public Collection getForbiddenMethods() {
+ return forbiddenMethods;
+ }
+
+ /**
+ * @return the events
+ */
+ public Collection getEvents() {
+ return events;
+ }
+
+ /**
+ * @return the usagePattern
+ */
+ public StateMachineGraph getUsagePattern() {
+ return usagePattern;
+ }
+
+ /**
+ * @return the constraints
+ */
+ public Collection getConstraints() {
+ return constraints;
+ }
+
+ /**
+ * @return the predicates
+ */
+ public Collection getPredicates() {
+ return predicates;
+ }
+
+ /**
+ * @return the negated predicates
+ */
+ public Collection getNegatedPredicates() {
+ return negatedPredicates;
+ }
+
+ /**
+ * @return the constraints
+ */
+ public Collection getRequiredPredicates() {
+ Collection requires = new LinkedList<>();
+ for (ISLConstraint con : constraints) {
+ if (con instanceof CrySLPredicate) {
+ requires.add((CrySLPredicate) con);
+ }
+ }
+ return requires;
+ }
+
+ @Override
+ public String toString() {
+ StringBuilder outputSB = new StringBuilder();
+
+ outputSB.append(this.className);
+
+ outputSB.append("\nforbiddenMethods:");
+ for (CrySLForbiddenMethod forMethSig : this.forbiddenMethods) {
+ outputSB.append(forMethSig);
+ outputSB.append(", ");
+ }
+
+ outputSB.append("\nEvents:");
+ for (CrySLMethod method : events) {
+ outputSB.append(method);
+ outputSB.append(", ");
+ }
+
+ outputSB.append("\nUsage Pattern:");
+ outputSB.append(this.usagePattern);
+
+ outputSB.append("\nConstraints:");
+ for (ISLConstraint constraint : this.constraints) {
+ outputSB.append(constraint);
+ outputSB.append(", ");
+ }
+
+ if (this.predicates != null) {
+ outputSB.append("\nPredicates:");
+ for (CrySLPredicate predicate : this.predicates) {
+ outputSB.append(predicate);
+ outputSB.append(", ");
+ }
+ }
+
+ if (this.negatedPredicates != null) {
+ outputSB.append("\nNegated predicates:");
+ for (CrySLPredicate predicate : this.negatedPredicates) {
+ outputSB.append(predicate);
+ outputSB.append(", ");
+ }
+ }
+
+ return outputSB.toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLSplitter.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLSplitter.java
new file mode 100644
index 0000000..f32a97c
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLSplitter.java
@@ -0,0 +1,32 @@
+package de.darmstadt.tu.crossing.rule;
+
+public class CrySLSplitter {
+
+ private final int index;
+ private final String split;
+
+ public CrySLSplitter(int ind, String spl) {
+ this.index = ind;
+ this.split = spl;
+ }
+
+ public int getIndex() {
+ return index;
+ }
+
+ public String getSplitter() {
+ return split;
+ }
+
+ @Override
+ public boolean equals(Object other) {
+ if (!(other instanceof CrySLSplitter)) return false;
+
+ CrySLSplitter splitter = (CrySLSplitter) other;
+ return this.index == splitter.getIndex() && this.split.equals(splitter.getSplitter());
+ }
+
+ public String toString() {
+ return ".split(" + split + ")[" + index + "]";
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLValueConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLValueConstraint.java
new file mode 100644
index 0000000..989f69e
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/CrySLValueConstraint.java
@@ -0,0 +1,60 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class CrySLValueConstraint extends CrySLLiteral {
+
+ CrySLObject var;
+ List valueRange;
+
+ public CrySLValueConstraint(CrySLObject name, List values) {
+ var = name;
+ valueRange = values;
+ }
+
+ /**
+ * @return the varName
+ */
+ public String getVarName() {
+ return var.getVarName();
+ }
+
+ /**
+ * @return the varName
+ */
+ public CrySLObject getVar() {
+ return var;
+ }
+
+ /**
+ * @return the valueRange
+ */
+ public List getValueRange() {
+ return valueRange;
+ }
+
+ public String toString() {
+ StringBuilder vCSB = new StringBuilder();
+ vCSB.append("VC:");
+ vCSB.append(var);
+ vCSB.append(" - ");
+ for (String value : valueRange) {
+ vCSB.append(value);
+ vCSB.append(",");
+ }
+ return vCSB.toString();
+ }
+
+ @Override
+ public List getInvolvedVarNames() {
+ List varNames = new ArrayList<>();
+ varNames.add(var.getVarName());
+ return varNames;
+ }
+
+ @Override
+ public String getName() {
+ return toString();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/FiniteStateMachine.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/FiniteStateMachine.java
new file mode 100644
index 0000000..2f16e4b
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/FiniteStateMachine.java
@@ -0,0 +1,11 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+
+public interface FiniteStateMachine {
+ Transition getInitialTransition();
+
+ Collection getAcceptingStates();
+
+ Collection> getAllTransitions();
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ICrySLPredicateParameter.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ICrySLPredicateParameter.java
new file mode 100644
index 0000000..6eca9d5
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ICrySLPredicateParameter.java
@@ -0,0 +1,6 @@
+package de.darmstadt.tu.crossing.rule;
+
+public interface ICrySLPredicateParameter {
+
+ String getName();
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ISLConstraint.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ISLConstraint.java
new file mode 100644
index 0000000..14d009b
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/ISLConstraint.java
@@ -0,0 +1,8 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.List;
+
+public interface ISLConstraint extends ICrySLPredicateParameter {
+
+ List getInvolvedVarNames();
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraph.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraph.java
new file mode 100644
index 0000000..83779cb
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraph.java
@@ -0,0 +1,189 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.stream.Collectors;
+
+public final class StateMachineGraph implements FiniteStateMachine {
+
+ private StateNode startNode;
+ private final Collection nodes;
+ private final Collection edges;
+ private final Collection initialEdges;
+ private int nodeNameCounter = 0;
+
+ public StateMachineGraph() {
+ nodes = new HashSet<>();
+ edges = new ArrayList<>();
+ initialEdges = new ArrayList<>();
+ }
+
+ public StateNode createNewNode() {
+ StateNode node = new StateNode(String.valueOf(this.nodeNameCounter++), false, false);
+ this.nodes.add(node);
+ return node;
+ }
+
+ public boolean createNewEdge(Collection methods, StateNode left, StateNode right) {
+ return this.addEdge(new TransitionEdge(methods, left, right));
+ }
+
+ private Boolean addEdge(TransitionEdge edge) {
+ final StateNode right = edge.getRight();
+ final StateNode left = edge.getLeft();
+ if (!(nodes.parallelStream().anyMatch(e -> e.equals(left))
+ || nodes.parallelStream().anyMatch(e -> e.equals(right)))) {
+ return false;
+ }
+ if (edges.contains(edge)) {
+ return false;
+ }
+ edges.add(edge);
+
+ if (left.isInitialState()) {
+ initialEdges.add(edge);
+ }
+
+ return true;
+ }
+
+ public void wrapUpCreation() {
+ getAcceptingStates().parallelStream()
+ .forEach(
+ e -> {
+ e.setHopsToAccepting(0);
+ updateHops(e);
+ });
+ }
+
+ public Collection getAllOutgoingEdges(StateNode node) {
+ return edges.parallelStream()
+ .filter(edge -> edge.from().equals(node))
+ .collect(Collectors.toSet());
+ }
+
+ public void addAllOutgoingEdgesFromOneNodeToOtherNodes(
+ StateNode node, Collection otherNodes) {
+ Collection edgesFromNode =
+ edges.parallelStream()
+ .filter(e -> node.equals(e.from()))
+ .collect(Collectors.toList());
+ otherNodes.forEach(
+ otherNode ->
+ edgesFromNode.forEach(
+ edge ->
+ this.createNewEdge(
+ edge.getLabel(), otherNode, edge.getLeft())));
+ }
+
+ public StateNode aggregateNodesToOneNode(Collection endNodes, StateNode newNode) {
+ this.aggregateNodesToOtherNodes(endNodes, Collections.singleton(newNode));
+ return newNode;
+ }
+
+ public Collection aggregateNodesToOtherNodes(
+ Collection nodesToAggr, Collection startNodes) {
+ Collection edgesToAnyAggrNode =
+ edges.parallelStream()
+ .filter(e -> nodesToAggr.contains(e.to()))
+ .collect(Collectors.toList());
+ // Add new edges to newNode instead of Aggr Node
+ startNodes.forEach(
+ node ->
+ edgesToAnyAggrNode.forEach(
+ edgeToAggrNode ->
+ this.createNewEdge(
+ edgeToAggrNode.getLabel(),
+ edgeToAggrNode.getLeft(),
+ node)));
+ nodesToAggr.removeAll(startNodes);
+ removeNodesWithAllEdges(nodesToAggr);
+ return startNodes;
+ }
+
+ private void removeNodesWithAllEdges(Collection nodesToRemove) {
+ nodesToRemove.forEach(this::removeNodeWithAllEdges);
+ }
+
+ private void removeNodeWithAllEdges(StateNode node) {
+ removeAllEdgesHavingNode(node);
+ nodes.remove(node);
+ }
+
+ private void removeAllEdgesHavingNode(StateNode node) {
+ Collection filteredEdges =
+ edges.parallelStream()
+ .filter(e -> node.equals(e.to()) || node.equals(e.from()))
+ .collect(Collectors.toList());
+ edges.removeAll(filteredEdges);
+ }
+
+ private void updateHops(StateNode node) {
+ int newPath = node.getHopsToAccepting() + 1;
+ getAllTransitions().parallelStream()
+ .forEach(
+ e -> {
+ StateNode theNewRight = e.getLeft();
+ if (e.getRight().equals(node)
+ && theNewRight.getHopsToAccepting() > newPath) {
+ theNewRight.setHopsToAccepting(newPath);
+ updateHops(theNewRight);
+ }
+ });
+ }
+
+ public Boolean addNode(StateNode node) {
+ if (node.isInitialState()) {
+ this.startNode = node;
+ }
+ return nodes.parallelStream().anyMatch(n -> n.getName().equals(node.getName()))
+ ? false
+ : nodes.add(node);
+ }
+
+ public String toString() {
+ StringBuilder graphSB = new StringBuilder();
+ for (StateNode node : nodes) {
+ graphSB.append(node.toString());
+ graphSB.append(System.lineSeparator());
+ }
+
+ for (TransitionEdge te : edges) {
+ graphSB.append(te.toString());
+ graphSB.append(System.lineSeparator());
+ }
+
+ return graphSB.toString();
+ }
+
+ public Collection getNodes() {
+ return nodes;
+ }
+
+ public StateNode getStartNode() {
+ return startNode;
+ }
+
+ public Collection getEdges() {
+ return edges;
+ }
+
+ public TransitionEdge getInitialTransition() {
+ throw new UnsupportedOperationException(
+ "There is no single initial transition. Use getInitialTransitions()");
+ }
+
+ public Collection getInitialTransitions() {
+ return initialEdges;
+ }
+
+ public Collection getAcceptingStates() {
+ return nodes.parallelStream().filter(StateNode::getAccepting).collect(Collectors.toList());
+ }
+
+ public Collection getAllTransitions() {
+ return getEdges();
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraphReader.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraphReader.java
new file mode 100644
index 0000000..13bfc1e
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateMachineGraphReader.java
@@ -0,0 +1,23 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.io.ObjectInputStream;
+
+public class StateMachineGraphReader {
+ public static StateMachineGraph readFromFile(File file) {
+ StateMachineGraph smg = null;
+ try {
+ FileInputStream fileIn = new FileInputStream(file);
+ ObjectInputStream in = new ObjectInputStream(fileIn);
+ smg = (StateMachineGraph) in.readObject();
+ System.err.println(smg);
+ in.close();
+ fileIn.close();
+ } catch (IOException | ClassNotFoundException e) {
+ e.printStackTrace();
+ }
+ return smg;
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateNode.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateNode.java
new file mode 100644
index 0000000..c7245f6
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/StateNode.java
@@ -0,0 +1,100 @@
+package de.darmstadt.tu.crossing.rule;
+
+public class StateNode {
+
+ private final String name;
+
+ private final Boolean init;
+ private Boolean accepting;
+ private int hopsToAccepting = Integer.MAX_VALUE;
+
+ public StateNode(String name) {
+ this(name, false, false);
+ }
+
+ public StateNode(String name, Boolean init) {
+ this(name, init, false);
+ }
+
+ public StateNode(String name, Boolean init, Boolean accepting) {
+ this.name = name;
+ this.init = init;
+ this.accepting = accepting;
+ }
+
+ public String getName() {
+ return name;
+ }
+
+ public Boolean getInit() {
+ return init;
+ }
+
+ public Boolean getAccepting() {
+ return accepting;
+ }
+
+ public void makeAccepting() {
+ this.accepting = true;
+ }
+
+ public void setAccepting(Boolean accepting) {
+ this.accepting = accepting;
+ }
+
+ public String toString() {
+ StringBuilder nodeSB = new StringBuilder();
+ nodeSB.append("Name: ");
+ nodeSB.append(name);
+ nodeSB.append(" (");
+ if (!accepting) {
+ nodeSB.append(hopsToAccepting + "hops to ");
+ }
+ nodeSB.append("accepting)");
+ return nodeSB.toString();
+ }
+
+ public boolean isErrorState() {
+ return !accepting;
+ }
+
+ public boolean isInitialState() {
+ return init;
+ }
+
+ @Override
+ public int hashCode() {
+ final int prime = 31;
+ int result = 1;
+ result = prime * result + ((accepting == null) ? 0 : accepting.hashCode());
+ result = prime * result + ((init == null) ? 0 : init.hashCode());
+ result = prime * result + ((name == null) ? 0 : name.hashCode());
+ return result;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) return true;
+ if (obj == null) return false;
+ if (getClass() != obj.getClass()) return false;
+ StateNode other = (StateNode) obj;
+ if (accepting == null) {
+ if (other.accepting != null) return false;
+ } else if (!accepting.equals(other.accepting)) return false;
+ if (init == null) {
+ if (other.init != null) return false;
+ } else if (!init.equals(other.init)) return false;
+ if (name == null) {
+ if (other.name != null) return false;
+ } else if (!name.equals(other.name)) return false;
+ return true;
+ }
+
+ public void setHopsToAccepting(int hops) {
+ hopsToAccepting = hops;
+ }
+
+ public int getHopsToAccepting() {
+ return hopsToAccepting;
+ }
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/Transition.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/Transition.java
new file mode 100644
index 0000000..e95e3e8
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/Transition.java
@@ -0,0 +1,11 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+
+public interface Transition {
+ State from();
+
+ State to();
+
+ Collection getLabel();
+}
diff --git a/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/TransitionEdge.java b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/TransitionEdge.java
new file mode 100644
index 0000000..aad7275
--- /dev/null
+++ b/CryslParser/src/main/java/de/darmstadt/tu/crossing/rule/TransitionEdge.java
@@ -0,0 +1,74 @@
+package de.darmstadt.tu.crossing.rule;
+
+import java.util.Collection;
+
+public class TransitionEdge implements Transition {
+
+ private final StateNode left;
+ private final StateNode right;
+ private final Collection methods;
+
+ public TransitionEdge(Collection _methods, StateNode _left, StateNode _right) {
+ left = _left;
+ right = _right;
+ methods = _methods;
+ }
+
+ public StateNode getLeft() {
+ return left;
+ }
+
+ public StateNode getRight() {
+ return right;
+ }
+
+ public Collection getLabel() {
+ return methods;
+ }
+
+ @Override
+ public String toString() {
+ return "Left: "
+ + this.left.getName()
+ + " ===="
+ + methods
+ + "====> Right:"
+ + this.right.getName();
+ }
+
+ public StateNode from() {
+ return left;
+ }
+
+ public StateNode to() {
+ return right;
+ }
+
+ @Override
+ public int hashCode() {
+ final int prime = 31;
+ int result = 1;
+ result = prime * result + ((methods == null) ? 0 : methods.hashCode());
+ result = prime * result + ((left == null) ? 0 : left.hashCode());
+ result = prime * result + ((right == null) ? 0 : right.hashCode());
+ return result;
+ }
+
+ @Override
+ public boolean equals(Object obj) {
+ if (this == obj) return true;
+ if (obj == null) return false;
+ if (getClass() != obj.getClass()) return false;
+ TransitionEdge other = (TransitionEdge) obj;
+ if (methods == null) {
+ if (other.methods != null) return false;
+ } else if (!methods.equals(other.methods)) return false;
+ if (left == null) {
+ if (other.left != null) return false;
+ } else if (!left.equals(other.left)) return false;
+ if (right == null) {
+ if (other.right != null) return false;
+ } else if (!right.equals(other.right)) return false;
+ return true;
+ }
+}
diff --git a/CryslParser/src/main/resources/plugin.properties b/CryslParser/src/main/resources/plugin.properties
new file mode 100644
index 0000000..5377da1
--- /dev/null
+++ b/CryslParser/src/main/resources/plugin.properties
@@ -0,0 +1,2 @@
+# Required by emf.core
+_UI_DiagnosticRoot_diagnostic=_UI_DiagnosticRoot_diagnostic
diff --git a/CryslParser/src/test/java/parser/CrySLParserTest.java b/CryslParser/src/test/java/parser/CrySLParserTest.java
new file mode 100644
index 0000000..28a231f
--- /dev/null
+++ b/CryslParser/src/test/java/parser/CrySLParserTest.java
@@ -0,0 +1,65 @@
+package parser;
+
+import de.darmstadt.tu.crossing.CrySLParser;
+import de.darmstadt.tu.crossing.rule.CrySLRule;
+import java.io.IOException;
+import java.util.Collection;
+import org.junit.Assert;
+import org.junit.Test;
+
+public class CrySLParserTest {
+
+ private static final String emptyZipFilePath = "src/test/resources/parser/empty.zip";
+ private static final String jcaRulesetZipFilePath =
+ "src/test/resources/parser/JavaCryptographicArchitecture-3.0.1-ruleset.zip";
+ private static final String junkRuleSet = "src/test/resources/parser/rulesetWithJunk.zip";
+
+ @Test
+ public void testNumberOfRules() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromPath(jcaRulesetZipFilePath);
+
+ Assert.assertEquals(49, rules.size());
+ }
+
+ @Test
+ public void testRulesZipFile() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromZipArchive(jcaRulesetZipFilePath);
+
+ Assert.assertEquals(49, rules.size());
+ }
+
+ @Test
+ public void testJunkThrows() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromPath(junkRuleSet);
+
+ Assert.assertEquals(48, rules.size());
+ }
+
+ @Test
+ public void testFileNoCrySLFiles() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromPath(emptyZipFilePath);
+
+ Assert.assertEquals(0, rules.size());
+ }
+
+ @Test(expected = IOException.class)
+ public void testFileNotExists() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromPath("notExist");
+ Assert.assertEquals(0, rules.size());
+ }
+
+ @Test
+ public void testRunTwiceSameResult() throws IOException {
+ CrySLParser parser = new CrySLParser();
+ Collection rules = parser.parseRulesFromPath(jcaRulesetZipFilePath);
+ Assert.assertEquals(49, rules.size());
+
+ rules = parser.parseRulesFromPath(jcaRulesetZipFilePath);
+ Assert.assertEquals(49, rules.size());
+ }
+}
diff --git a/CryslParser/src/test/java/statemachine/StateMachineTest.java b/CryslParser/src/test/java/statemachine/StateMachineTest.java
new file mode 100644
index 0000000..8a4960d
--- /dev/null
+++ b/CryslParser/src/test/java/statemachine/StateMachineTest.java
@@ -0,0 +1,76 @@
+package statemachine;
+
+import de.darmstadt.tu.crossing.CrySLParser;
+import de.darmstadt.tu.crossing.parsing.CrySLException;
+import de.darmstadt.tu.crossing.rule.CrySLRule;
+import de.darmstadt.tu.crossing.rule.StateMachineGraph;
+import de.darmstadt.tu.crossing.rule.TransitionEdge;
+import java.io.File;
+import java.util.Collection;
+import org.junit.Assert;
+import org.junit.Test;
+
+public class StateMachineTest {
+
+ private static final String TEST_PATH =
+ "."
+ + File.separator
+ + "src"
+ + File.separator
+ + "test"
+ + File.separator
+ + "resources"
+ + File.separator
+ + "stateMachineRules"
+ + File.separator;
+ private static final String CRYSL_FILE = "StateMachineTester.crysl";
+
+ @Test
+ public void testOptionalAfterStar() {
+ // (Op1?, Op2, Op3)*
+ StateMachineGraph smg = getStateMachineGraph("optionalAfterStar");
+ Collection edges = smg.getEdges();
+
+ Assert.assertEquals(edges.size(), 7);
+ Assert.assertTrue(stateMachineContainsEdge("0", "1", edges));
+ Assert.assertTrue(stateMachineContainsEdge("0", "2", edges));
+ Assert.assertTrue(stateMachineContainsEdge("3", "1", edges));
+ Assert.assertTrue(stateMachineContainsEdge("3", "2", edges));
+ }
+
+ @Test
+ public void testOptionalBetweenStar() {
+ // (Op1, Op2?, Op3)*
+ StateMachineGraph smg = getStateMachineGraph("optionalBetweenStar");
+ Collection edges = smg.getEdges();
+
+ Assert.assertEquals(edges.size(), 6);
+ Assert.assertTrue(stateMachineContainsEdge("1", "2", edges));
+ Assert.assertTrue(stateMachineContainsEdge("1", "3", edges));
+ Assert.assertTrue(stateMachineContainsEdge("3", "1", edges));
+ Assert.assertFalse(stateMachineContainsEdge("3", "2", edges));
+ }
+
+ private StateMachineGraph getStateMachineGraph(String ruleName) {
+ try {
+ CrySLParser parser = new CrySLParser();
+
+ CrySLRule rule =
+ parser.parseRuleFromFile(
+ new File(TEST_PATH + ruleName + File.separator + CRYSL_FILE));
+ return rule.getUsagePattern();
+ } catch (CrySLException e) {
+ throw new RuntimeException("Unable to find rules for " + ruleName, e);
+ }
+ }
+
+ private boolean stateMachineContainsEdge(
+ String from, String to, Collection edges) {
+ for (TransitionEdge edge : edges) {
+ if (edge.from().getName().equals(from) && edge.to().getName().equals(to)) {
+ return true;
+ }
+ }
+ return false;
+ }
+}
diff --git a/CryslParser/src/test/java/statemachine/StateMachineTester.java b/CryslParser/src/test/java/statemachine/StateMachineTester.java
new file mode 100644
index 0000000..aeec9c0
--- /dev/null
+++ b/CryslParser/src/test/java/statemachine/StateMachineTester.java
@@ -0,0 +1,12 @@
+package statemachine;
+
+public class StateMachineTester {
+
+ public void operation1() {}
+
+ public void operation2() {}
+
+ public void operation3() {}
+
+ public void operation4() {}
+}
diff --git a/CryslParser/src/test/resources/parser/JavaCryptographicArchitecture-3.0.1-ruleset.zip b/CryslParser/src/test/resources/parser/JavaCryptographicArchitecture-3.0.1-ruleset.zip
new file mode 100644
index 0000000..a9f6145
Binary files /dev/null and b/CryslParser/src/test/resources/parser/JavaCryptographicArchitecture-3.0.1-ruleset.zip differ
diff --git a/CryslParser/src/test/resources/parser/Multiple-rulesets.zip b/CryslParser/src/test/resources/parser/Multiple-rulesets.zip
new file mode 100644
index 0000000..1eb076c
Binary files /dev/null and b/CryslParser/src/test/resources/parser/Multiple-rulesets.zip differ
diff --git a/CryslParser/src/test/resources/parser/empty.zip b/CryslParser/src/test/resources/parser/empty.zip
new file mode 100644
index 0000000..15cb0ec
Binary files /dev/null and b/CryslParser/src/test/resources/parser/empty.zip differ
diff --git a/CryslParser/src/test/resources/parser/rulesetWithJunk.zip b/CryslParser/src/test/resources/parser/rulesetWithJunk.zip
new file mode 100644
index 0000000..8bfa125
Binary files /dev/null and b/CryslParser/src/test/resources/parser/rulesetWithJunk.zip differ
diff --git a/CryslParser/src/test/resources/stateMachineRules/optionalAfterStar/StateMachineTester.crysl b/CryslParser/src/test/resources/stateMachineRules/optionalAfterStar/StateMachineTester.crysl
new file mode 100644
index 0000000..e687027
--- /dev/null
+++ b/CryslParser/src/test/resources/stateMachineRules/optionalAfterStar/StateMachineTester.crysl
@@ -0,0 +1,11 @@
+SPEC statemachine.StateMachineTester
+
+EVENTS
+ Con: StateMachineTester();
+ Op1: operation1();
+ Op2: operation2();
+ Op3: operation3();
+ Op4: operation4();
+
+ORDER
+ Con, (Op1?, Op2, Op3)*
diff --git a/CryslParser/src/test/resources/stateMachineRules/optionalBetweenStar/StateMachineTester.crysl b/CryslParser/src/test/resources/stateMachineRules/optionalBetweenStar/StateMachineTester.crysl
new file mode 100644
index 0000000..74a1483
--- /dev/null
+++ b/CryslParser/src/test/resources/stateMachineRules/optionalBetweenStar/StateMachineTester.crysl
@@ -0,0 +1,11 @@
+SPEC statemachine.StateMachineTester
+
+EVENTS
+ Con: StateMachineTester();
+ Op1: operation1();
+ Op2: operation2();
+ Op3: operation3();
+ Op4: operation4();
+
+ORDER
+ Con, (Op1, Op2?, Op3)*
diff --git a/de.darmstadt.tu.crossing.CrySL/pom.xml b/de.darmstadt.tu.crossing.CrySL/pom.xml
index 80fae9b..cc41351 100644
--- a/de.darmstadt.tu.crossing.CrySL/pom.xml
+++ b/de.darmstadt.tu.crossing.CrySL/pom.xml
@@ -33,7 +33,6 @@
-
diff --git a/pom.xml b/pom.xml
index 1a76fa5..f94d347 100644
--- a/pom.xml
+++ b/pom.xml
@@ -25,6 +25,7 @@
+ CrySLParser
de.darmstadt.tu.crossing.CrySL
de.darmstadt.tu.crossing.CrySL.ide
de.darmstadt.tu.crossing.CrySL.ui
@@ -55,12 +56,10 @@
2.35.0
2.19.0
UTF-8
- 1.8
- 1.8
+ 11
-