Skip to content
Snippets Groups Projects
Commit a978a0a2 authored by dgelessus's avatar dgelessus
Browse files

Remove unused packages that seem to be old ProB 2 code

parent a37d1e2c
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 0 additions and 709 deletions
de.prob.core/META-INF/MANIFEST.MF
+ 0
− 4
View file @ a978a0a2
......@@ -59,7 +59,6 @@ Export-Package: com.thoughtworks.xstream,
de.be4.ltl.core.parser.node,
de.be4.ltl.core.parser.parser,
de.hhu.stups.sablecc.patch,
de.prob.animator.domainobjects,
de.prob.cli,
de.prob.cli.clipatterns,
de.prob.core,
......@@ -83,9 +82,6 @@ Export-Package: com.thoughtworks.xstream,
de.prob.eventb.translator.internal,
de.prob.exceptions,
de.prob.logging,
de.prob.model.eventb,
de.prob.model.representation,
de.prob.model.serialize,
de.prob.parser,
de.prob.parserbase,
de.prob.prolog.match,
......
de.prob.core/src/de/prob/animator/domainobjects/EvalElementType.java deleted 100644 → 0
+ 0
− 11
View file @ a37d1e2c
package de.prob.animator.domainobjects;
public enum EvalElementType {
PREDICATE, EXPRESSION;
@Override
public String toString() {
return "#" + super.toString();
}
}
de.prob.core/src/de/prob/animator/domainobjects/EvaluationResult.java deleted 100644 → 0
+ 0
− 102
View file @ a37d1e2c
package de.prob.animator.domainobjects;
import java.util.Arrays;
import java.util.List;
/**
* This is what is saved when a formula ({@link IEvalElement}) is executed in
* the StateSpace
*
* @author joy
*
*/
public class EvaluationResult {
public final String value;
public final String solution;
public final String errors;
public final String code;
public final String explanation;
private final String resultType;
private final List<String> quantifiedVars;
private final boolean enumerationWarnings;
private final String stateid;
public EvaluationResult(final String stateid, final String code,
final String value, final String solution, final String errors,
final String resultType, final List<String> quantifiedVars,
final boolean enumerationWarnings) {
this.stateid = stateid;
this.code = code;
this.value = value;
this.solution = solution;
this.errors = errors;
this.resultType = resultType;
this.quantifiedVars = quantifiedVars;
this.enumerationWarnings = enumerationWarnings;
if (!solutionMode(resultType) && "TRUE".equals(value)) {
this.explanation = "Solution";
} else {
this.explanation = solutionMode(resultType) ? " Solution: "
: " Counterexample: ";
}
}
public EvaluationResult(final String stateid, final String code,
final String value, final String solution, final String errors,
final String resultType, final String[] strings,
final boolean enumerationWarnings) {
this(stateid, code, value, solution, errors, resultType, Arrays
.asList(strings), enumerationWarnings);
}
private boolean solutionMode(final String arg0) {
return "exists".equals(arg0);
}
public String getResultType() {
return resultType;
}
public List<String> getQuantifiedVars() {
return quantifiedVars;
}
public boolean hasEnumerationWarnings() {
return enumerationWarnings;
}
public boolean hasError() {
return errors != null && !errors.isEmpty(); // You're kidding, aren't
// you? ;-)
}
public String getErrors() {
return errors;
}
public String getValue() {
return value;
}
@Override
public String toString() {
final String result;
if (hasError()) {
result = "'Errors: " + errors + "'";
} else {
result = (solution == null || solution.equals("")) ? value : value
+ explanation + solution;
}
return result;
}
public String getStateId() {
return stateid;
}
public String getStateid() {
return stateid;
}
}
de.prob.core/src/de/prob/animator/domainobjects/EventB.java deleted 100644 → 0
+ 0
− 114
View file @ a37d1e2c
package de.prob.animator.domainobjects;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.Node;
import de.prob.model.representation.FormulaUUID;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.unicode.UnicodeTranslator;
/**
* Representation of an Event-B formula
*
* @author joy
*
*/
public class EventB implements IEvalElement {
public FormulaUUID uuid = new FormulaUUID();
private final String code;
private String kind;
private Node ast = null;
/**
* @param code
* - The String which is a representation of the desired Event-B
* formula
*/
public EventB(final String code) {
this.code = UnicodeTranslator.toAscii(code);
}
private void ensureParsed() {
// final String unicode = UnicodeTranslator.toUnicode(code);
// kind = PREDICATE.toString();
// IParseResult parseResult =
// FormulaFactory.getDefault().parsePredicate(
// unicode, LanguageVersion.LATEST, null);
//
// if (!parseResult.hasProblem()) {
// ast = preparePredicateAst(parseResult);
//
// } else {
// kind = EXPRESSION.toString();
// parseResult = FormulaFactory.getDefault().parseExpression(unicode,
// LanguageVersion.LATEST, null);
// ast = prepareExpressionAst(parseResult);
// }
// if (parseResult.hasProblem()) {
// throwException(code, parseResult);
// }
}
// private Node prepareExpressionAst(final IParseResult parseResult) {
// final Expression expr = parseResult.getParsedExpression();
// final ExpressionVisitor visitor = new ExpressionVisitor(
// new LinkedList<String>());
// expr.accept(visitor);
// final Node expression = visitor.getExpression();
// return expression;
// }
//
// private Node preparePredicateAst(final IParseResult parseResult) {
// final Predicate parsedPredicate = parseResult.getParsedPredicate();
// final PredicateVisitor visitor = new PredicateVisitor();
// parsedPredicate.accept(visitor);
// return visitor.getPredicate();
// }
//
// private void throwException(final String code,
// final IParseResult parseResult) {
// final List<ASTProblem> problems = parseResult.getProblems();
// final ArrayList<String> msgs = new ArrayList<String>();
// for (final ASTProblem astProblem : problems) {
// msgs.add(astProblem.getMessage().toString());
// }
// final String error = Joiner.on(", \n").join(msgs);
// throw new EvaluationException("Cannot parse " + code + ":\n " + error);
// }
@Override
public String getCode() {
return code;
}
@Override
public boolean equals(final Object that) {
if (that instanceof EventB) {
return ((EventB) that).getCode().equals(this.getCode());
}
return false;
}
@Override
public void printProlog(final IPrologTermOutput pout) {
if (ast == null) {
ensureParsed();
}
assert ast != null;
final ASTProlog prolog = new ASTProlog(pout, null);
ast.apply(prolog);
}
@Override
public String getKind() {
return kind;
}
@Override
public String toString() {
return getCode();
}
}
de.prob.core/src/de/prob/animator/domainobjects/IEvalElement.java deleted 100644 → 0
+ 0
− 11
View file @ a37d1e2c
package de.prob.animator.domainobjects;
import de.prob.prolog.output.IPrologTermOutput;
public interface IEvalElement {
public abstract String getCode();
public abstract void printProlog(IPrologTermOutput pout);
public abstract String getKind();
}
de.prob.core/src/de/prob/model/eventb/Context.java deleted 100644 → 0
+ 0
− 41
View file @ a37d1e2c
package de.prob.model.eventb;
import java.util.List;
import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.Axiom;
import de.prob.model.representation.BSet;
import de.prob.model.representation.Constant;
public class Context extends AbstractElement {
private final String name;
public Context(final String name) {
this.name = name;
}
public String getName() {
return name;
}
public void addExtends(final List<Context> contexts) {
put(Context.class, contexts);
}
public void addSets(final List<BSet> sets) {
put(BSet.class, sets);
}
public void addConstants(final List<EventBConstant> constants) {
put(Constant.class, constants);
}
public void addAxioms(final List<EventBAxiom> axioms) {
put(Axiom.class, axioms);
}
@Override
public String toString() {
return name;
}
}
de.prob.core/src/de/prob/model/eventb/Event.java deleted 100644 → 0
+ 0
− 75
View file @ a37d1e2c
package de.prob.model.eventb;
import java.util.List;
import java.util.Set;
import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.Action;
import de.prob.model.representation.BEvent;
import de.prob.model.representation.Guard;
public class Event extends BEvent {
private final EventType type;
public enum EventType {
ORDINARY, CONVERGENT, ANTICIPATED
}
public Event(final String name, final EventType type) {
super(name);
this.type = type;
}
public void addRefines(final List<Event> refines) {
put(Event.class, refines);
}
public void addGuards(final List<EventBGuard> guards) {
put(Guard.class, guards);
}
public void addActions(final List<EventBAction> actions) {
put(Action.class, actions);
}
public void addWitness(final List<Witness> witness) {
put(Witness.class, witness);
}
public void addParameters(final List<EventParameter> parameters) {
put(EventParameter.class, parameters);
}
public EventType getType() {
return type;
}
@Override
public String toString() {
return getName();
}
public String print() {
StringBuilder sb = new StringBuilder();
sb.append("Name: " + getName() + "\n");
sb.append("Type: " + type.toString() + "\n");
addChildren("Refines", getChildrenOfType(Event.class), sb);
addChildren("Any", getChildrenOfType(EventParameter.class), sb);
addChildren("Where", getChildrenOfType(Guard.class), sb);
addChildren("With", getChildrenOfType(Witness.class), sb);
addChildren("Then", getChildrenOfType(Action.class), sb);
return sb.toString();
}
private void addChildren(final String name,
final Set<? extends AbstractElement> childrenOfType,
final StringBuilder sb) {
if (!childrenOfType.isEmpty()) {
sb.append(name + ": \n");
for (AbstractElement abstractElement : childrenOfType) {
sb.append("\t" + abstractElement.toString() + "\n");
}
}
}
}
de.prob.core/src/de/prob/model/eventb/EventBAction.java deleted 100644 → 0
+ 0
− 22
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.model.representation.Action;
public class EventBAction extends Action {
private final String name;
public EventBAction(final String name, final String code) {
super(code);
this.name = name;
}
public String getName() {
return name;
}
@Override
public String toString() {
return name + ": " + getCode();
}
}
de.prob.core/src/de/prob/model/eventb/EventBAxiom.java deleted 100644 → 0
+ 0
− 25
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.model.representation.Axiom;
public class EventBAxiom extends Axiom {
private final String name;
private final boolean theorem;
public EventBAxiom(final String name, final String code,
final boolean theorem) {
super(new EventB(code));
this.name = name;
this.theorem = theorem;
}
public String getName() {
return name;
}
public boolean isTheorem() {
return theorem;
}
}
de.prob.core/src/de/prob/model/eventb/EventBConstant.java deleted 100644 → 0
+ 0
− 18
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.model.representation.Constant;
public class EventBConstant extends Constant {
private final String name;
public EventBConstant(final String name) {
super(new EventB(name));
this.name = name;
}
public String getName() {
return name;
}
}
de.prob.core/src/de/prob/model/eventb/EventBGuard.java deleted 100644 → 0
+ 0
− 25
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.model.representation.Guard;
public class EventBGuard extends Guard {
private final String name;
private final boolean theorem;
public EventBGuard(final String name, final String code,
final boolean theorem) {
super(new EventB(code));
this.name = name;
this.theorem = theorem;
}
public String getName() {
return name;
}
public boolean isTheorem() {
return theorem;
}
}
de.prob.core/src/de/prob/model/eventb/EventBInvariant.java deleted 100644 → 0
+ 0
− 25
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.model.representation.Invariant;
public class EventBInvariant extends Invariant {
private final String name;
private final boolean theorem;
public EventBInvariant(final String name, final String code,
final boolean theorem) {
super(new EventB(code));
this.name = name;
this.theorem = theorem;
}
public String getName() {
return name;
}
public boolean isTheorem() {
return theorem;
}
}
de.prob.core/src/de/prob/model/eventb/EventBMachine.java deleted 100644 → 0
+ 0
− 38
View file @ a37d1e2c
package de.prob.model.eventb;
import java.util.List;
import de.prob.model.representation.BEvent;
import de.prob.model.representation.Invariant;
import de.prob.model.representation.Machine;
import de.prob.model.representation.Variable;
public class EventBMachine extends Machine {
public EventBMachine(final String name) {
super(name);
}
public void addRefines(final List<EventBMachine> refines) {
put(Machine.class, refines);
}
public void addSees(final List<Context> sees) {
put(Context.class, sees);
}
public void addVariables(final List<EventBVariable> variables) {
put(Variable.class, variables);
}
public void addInvariants(final List<EventBInvariant> invariants) {
put(Invariant.class, invariants);
}
public void addVariant(final List<Variant> variant) {
put(Variant.class, variant);
}
public void addEvents(final List<Event> events) {
put(BEvent.class, events);
}
}
de.prob.core/src/de/prob/model/eventb/EventBVariable.java deleted 100644 → 0
+ 0
− 18
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.model.representation.Variable;
public class EventBVariable extends Variable {
private final String name;
public EventBVariable(final String name) {
super(new EventB(name));
this.name = name;
}
public String getName() {
return name;
}
}
de.prob.core/src/de/prob/model/eventb/EventParameter.java deleted 100644 → 0
+ 0
− 22
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.model.representation.AbstractElement;
public class EventParameter extends AbstractElement {
private final String name;
public EventParameter(final String name) {
this.name = name;
}
public String getName() {
return name;
}
@Override
public String toString() {
return name;
}
}
de.prob.core/src/de/prob/model/eventb/Variant.java deleted 100644 → 0
+ 0
− 23
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.IEval;
public class Variant extends AbstractElement implements IEval {
private final IEvalElement expression;
public Variant(final String code) {
expression = new EventB(code);
}
public IEvalElement getExpression() {
return expression;
}
@Override
public IEvalElement getEvaluate() {
return expression;
}
}
de.prob.core/src/de/prob/model/eventb/Witness.java deleted 100644 → 0
+ 0
− 31
View file @ a37d1e2c
package de.prob.model.eventb;
import de.prob.animator.domainobjects.EventB;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.model.representation.AbstractElement;
import de.prob.model.representation.IEval;
public class Witness extends AbstractElement implements IEval {
private final String name;
private final EventB predicate;
public Witness(final String name, final String code) {
this.name = name;
predicate = new EventB(code);
}
public String getName() {
return name;
}
public EventB getPredicate() {
return predicate;
}
@Override
public IEvalElement getEvaluate() {
return predicate;
}
}
de.prob.core/src/de/prob/model/representation/AbstractElement.java deleted 100644 → 0
+ 0
− 58
View file @ a37d1e2c
package de.prob.model.representation;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Set;
/**
* This class is the subclass of all model elements (Models, Machines, Contexts,
* Variables, etc.)
*
* @author joy
*
*/
public abstract class AbstractElement {
protected Map<Class<? extends AbstractElement>, java.util.Set<? extends AbstractElement>> children = new HashMap<Class<? extends AbstractElement>, Set<? extends AbstractElement>>();
/**
* Each {@link AbstractElement} can have children of a subclass that extends
* {@link AbstractElement}. These are specified by the class of the child.
* To get a Set of all of the children of a particular class, use this
* method.
*
* @param c
* {@link Class} T of the desired type of children
* @return {@link Set} containing all the children of type T
*/
@SuppressWarnings("unchecked")
public <T extends AbstractElement> Set<T> getChildrenOfType(final Class<T> c) {
Set<? extends AbstractElement> set = children.get(c);
if (set == null) {
return Collections.emptySet();
}
return (Set<T>) set;
}
/**
* Maps a {@link Collection} of elements to the specified {@link Class}
*
* @param c
* {@link Class} to specify children elements
* @param elements
* {@link Collection} of elements with which c will be mapped
*/
public <T extends AbstractElement> void put(final Class<T> c,
final Collection<? extends T> elements) {
children.put(c, new LinkedHashSet<T>(elements));
}
/**
* @return the {@link Map} of {@link Class} to {@link Set} of children
*/
public Map<Class<? extends AbstractElement>, java.util.Set<? extends AbstractElement>> getChildren() {
return children;
}
}
de.prob.core/src/de/prob/model/representation/Action.java deleted 100644 → 0
+ 0
− 19
View file @ a37d1e2c
package de.prob.model.representation;
public abstract class Action extends AbstractElement {
private final String code;
public Action(final String code) {
this.code = code;
}
public String getCode() {
return code;
}
@Override
public String toString() {
return code;
}
}
de.prob.core/src/de/prob/model/representation/Axiom.java deleted 100644 → 0
+ 0
− 27
View file @ a37d1e2c
package de.prob.model.representation;
import de.prob.animator.domainobjects.IEvalElement;
import de.prob.unicode.UnicodeTranslator;
public abstract class Axiom extends AbstractElement implements IEval {
private final IEvalElement predicate;
public Axiom(final IEvalElement predicate) {
this.predicate = predicate;
}
public IEvalElement getPredicate() {
return predicate;
}
@Override
public IEvalElement getEvaluate() {
return predicate;
}
@Override
public String toString() {
return UnicodeTranslator.toUnicode(predicate.getCode());
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment