Skip to content
Snippets Groups Projects
Commit 9658b395 authored by hansen's avatar hansen
Browse files

Resolving generated names of MC.tla files

parent a8418bab
No related branches found
No related tags found
No related merge requests found
......@@ -395,8 +395,6 @@ public class TypeChecker extends BuiltInOPs implements IType, ASTConstants,
}else{
throw new RuntimeException(vName + " has no type yet!");
}
}
try {
TLAType result = expected.unify(v);
......
......@@ -2,7 +2,6 @@ package de.tla2bAst;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.LinkedList;
......@@ -182,7 +181,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
this.specAnalyser = specAnalyser;
this.bMacroHandler = new BMacroHandler();
this.predicateVsExpression = new PredicateVsExpression(moduleNode);
this.recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
this.recursiveFunctionHandler = new RecursiveFunctionHandler(
specAnalyser);
ExprNode expr = moduleNode.getOpDefs()[moduleNode.getOpDefs().length - 1]
.getBody();
......@@ -289,6 +289,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
.containsValue(def)) {
continue;
}
if (def.getOriginallyDefinedInModuleNode().getName().toString()
.equals("MC")) {
continue;
}
bDefs.add(def);
}
......@@ -695,8 +700,6 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private void createInvariantClause() {
OpDeclNode[] vars = moduleNode.getVariableDecls();
if (vars.length == 0)
return;
List<PPredicate> predList = new ArrayList<PPredicate>();
for (int i = 0; i < vars.length; i++) {
......@@ -711,17 +714,25 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
if (conEval != null) {
for (OpDefNode def : conEval.getInvariants()) {
if (def.getOriginallyDefinedInModuleNode().getName().toString()
.equals("MC")) {
predList.add(visitExprNodePredicate(def.getBody()));
} else {
ADefinitionPredicate defPred = new ADefinitionPredicate();
defPred.setDefLiteral(new TDefLiteralPredicate(getName(def)));
predList.add(defPred);
}
}
}
if (predList.size() > 0) {
AInvariantMachineClause invClause = new AInvariantMachineClause(
createConjunction(predList));
machineClauseList.add(invClause);
}
}
private PPredicate visitAssumeNode(AssumeNode assumeNode) {
return visitExprNodePredicate(assumeNode.getAssume());
}
......
/*@ generated by TLA2B 1.0.7 Fri May 09 16:29:56 CEST 2014 */
MACHINE Club
SETS ENUM1 = {n1, n2, n3}
ABSTRACT_CONSTANTS capacity, NAME, total
PROPERTIES
((((capacity : INTEGER & NAME = ENUM1) & total : INTEGER) & (capacity : NATURAL & capacity = 2)) & card(NAME) > capacity) & (total : NATURAL & total > 2)
VARIABLES member, waiting
INVARIANT
member : POW(ENUM1) & waiting : POW(ENUM1)
INITIALISATION
member, waiting:(member = {} & waiting = {})
OPERATIONS
join_queue(nn) = ANY member_n WHERE ((((nn : NAME & nn /: member) & nn /: waiting) & member_n : POW(ENUM1)) & card(waiting) < total) & member_n = member THEN waiting,member := waiting \/ {nn},member_n END;
join(nn) = SELECT ((nn : NAME & nn : waiting) & card(member) < capacity) & card(member) < capacity THEN member,waiting := member \/ {nn},waiting - {nn} END;
remove(nn) = ANY waiting_n WHERE ((nn : NAME & nn : member) & waiting_n : POW(ENUM1)) & waiting_n = waiting THEN member,waiting := member - {nn},waiting_n END
END
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment