diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 6496f4cef454dfdeda39249dd7142f370125aa92..0f8f0c259191e6338f075c296c5b1d7b7748ff8d 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -20,7 +20,7 @@ public class RecursiveFunktion extends BuiltInOPs {
throws NotImplementedException {
def = n;
this.rfs = rfs;
- evalDef();
+ //evalDef();
}
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 45c28d535dd540bcc791114628bcdff714dc703a..7602508f2295ea4a7a62092ec2618145951d7190 100644
--- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java
+++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
@@ -70,7 +70,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
// surrounding operator
private ArrayList<String> definitionMacros = new ArrayList<String>();
- private ArrayList<RecursiveFunktion> recursiveFunctions = new ArrayList<RecursiveFunktion>();
+ private ArrayList<OpDefNode> recursiveFunctions = new ArrayList<OpDefNode>();
private ArrayList<RecursiveDefinition> recursiveDefinitions = new ArrayList<RecursiveDefinition>();
@@ -578,9 +578,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
switch (getOpCode(o.getOperator().getName())) {
case OPCODE_rfs: { // recursive Function
bDefinitionsSet.remove(def);
- ifThenElseNodes.remove(o.getArgs()[0]);
- RecursiveFunktion rf = new RecursiveFunktion(def, o);
- recursiveFunctions.add(rf);
+ recursiveFunctions.add(def);
return;
}
}
@@ -588,17 +586,17 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
}
}
- public void evalIfThenElse() {
- boolean b = false;
- for (int i = 0; i < ifThenElseNodes.size() && !b; i++) {
- OpApplNode node = ifThenElseNodes.get(i);
- TLAType t = (TLAType) node.getToolObject(TYPE_ID);
- if (t.getKind() != BOOL)
- b = true;
- }
- if (b)
- definitionMacros.add(IF_THEN_ELSE);
- }
+// public void evalIfThenElse() {
+// boolean b = false;
+// for (int i = 0; i < ifThenElseNodes.size() && !b; i++) {
+// OpApplNode node = ifThenElseNodes.get(i);
+// TLAType t = (TLAType) node.getToolObject(TYPE_ID);
+// if (t.getKind() != BOOL)
+// b = true;
+// }
+// if (b)
+// definitionMacros.add(IF_THEN_ELSE);
+// }
public ArrayList<LetInNode> getGlobalLets() {
return this.globalLets;
@@ -632,7 +630,7 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
return usedDefinitions;
}
- public ArrayList<RecursiveFunktion> getRecursiveFunctions() {
+ public ArrayList<OpDefNode> getRecursiveFunctions() {
return recursiveFunctions;
}
diff --git a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
index c73b870bb6438b4cc2f2dfa43a3b00535188d8ee..8fabe8f168cdae4700e6f5bd8e1a2e53064c68d4 100644
--- a/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
+++ b/src/main/java/de/tla2b/analysis/UsedExternalFunctions.java
@@ -1,21 +1,15 @@
package de.tla2b.analysis;
import java.util.HashSet;
-import java.util.Hashtable;
import java.util.Set;
-import tla2sany.semantic.ASTConstants;
-import tla2sany.semantic.AssumeNode;
import tla2sany.semantic.ExprNode;
import tla2sany.semantic.ExprOrOpArgNode;
-import tla2sany.semantic.LetInNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpApplNode;
import tla2sany.semantic.OpDefNode;
-import tla2sany.semantic.SemanticNode;
-import tlc2.tool.BuiltInOPs;
-public class UsedExternalFunctions extends BuiltInOPs implements ASTConstants {
+public class UsedExternalFunctions extends AbstractASTVisitor {
public enum EXTERNAL_FUNCTIONS {
CHOOSE
@@ -31,65 +25,34 @@ public class UsedExternalFunctions extends BuiltInOPs implements ASTConstants {
SpecAnalyser specAnalyser) {
usedExternalFunctions = new HashSet<UsedExternalFunctions.EXTERNAL_FUNCTIONS>();
- AssumeNode[] assumes = moduleNode.getAssumptions();
- for (int i = 0; i < assumes.length; i++) {
- AssumeNode assume = assumes[i];
- visitSemanticNode(assume.getAssume());
- }
+ visitAssumptions(moduleNode.getAssumptions());
for (OpDefNode def : specAnalyser.getUsedDefinitions()) {
- visitSemanticNode(def.getBody());
+ visitDefinition(def);
}
}
- private void findExternalFunctions(Hashtable<Integer, SemanticNode> table) {
- for (SemanticNode sNode : table.values()) {
- if (sNode instanceof OpApplNode) {
- OpApplNode opApplNode = (OpApplNode) sNode;
- int kind = opApplNode.getOperator().getKind();
- if (kind == BuiltInKind) {
- switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_case: {
- usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
- }
- case OPCODE_bc: {
- usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
- }
- }
-
- }
- }
+ @Override
+ public void visitBuiltInNode(OpApplNode n) {
+ switch (getOpCode(n.getOperator().getName())) {
+ case OPCODE_case:
+ case OPCODE_uc:
+ case OPCODE_bc: {
+ usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+ }
}
- }
-
- private void visitSemanticNode(SemanticNode s) {
- if (s == null)
- return;
- if (s instanceof OpApplNode) {
- OpApplNode opApplNode = (OpApplNode) s;
- int kind = opApplNode.getOperator().getKind();
- if (kind == BuiltInKind) {
- switch (getOpCode(opApplNode.getOperator().getName())) {
- case OPCODE_case:
- case OPCODE_bc:
- case OPCODE_uc: {
- usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
- break;
- }
- }
-
- }
- for (SemanticNode arg : opApplNode.getArgs()) {
- visitSemanticNode(arg);
- }
+ ExprNode[] in = n.getBdedQuantBounds();
+ for (ExprNode exprNode : in) {
+ visitExprNode(exprNode);
}
- SemanticNode[] children = s.getChildren();
- if (children != null) {
- for (SemanticNode semanticNode : children) {
- visitSemanticNode(semanticNode);
+ ExprOrOpArgNode[] arguments = n.getArgs();
+ for (ExprOrOpArgNode exprOrOpArgNode : arguments) {
+ // exprOrOpArgNode == null in case the OTHER construct
+ if (exprOrOpArgNode != null) {
+ visitExprOrOpArgNode(exprOrOpArgNode);
}
}
}
diff --git a/src/main/java/de/tla2b/pprint/BMachinePrinter.java b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
index 952d3923019cee23e29f4287fcff3ddfb47fe8e3..f9499be280814826142d90b47f56b3ac48399c86 100644
--- a/src/main/java/de/tla2b/pprint/BMachinePrinter.java
+++ b/src/main/java/de/tla2b/pprint/BMachinePrinter.java
@@ -77,7 +77,7 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
this.definitionMacro = specAnalyser.getDefinitionMacros();
this.bDefinitions = specAnalyser.getBDefinitions();
this.letParams = specAnalyser.getLetParams();
- this.recursiveFunktions = specAnalyser.getRecursiveFunctions();
+ //this.recursiveFunktions = specAnalyser.getRecursiveFunctions();
}
public StringBuilder start() {
@@ -139,69 +139,69 @@ public class BMachinePrinter extends AbstractExpressionPrinter implements
continue;
if (!printed.contains(e)) {
- e.id = counter;
- if (!first) {
- out.append("; ");
- }
- out.append("ENUM" + counter + " = {");
- Iterator<String> it2 = e.modelvalues.iterator();
- while (it2.hasNext()) {
- out.append(it2.next());
- if (it2.hasNext()) {
- out.append(", ");
- }
- }
- if (e.hasNoVal()) {
- out.append(", noVal" + counter);
- }
- out.append("}");
- printed.add(e);
- counter++;
- first = false;
+ //e.id = counter;
+// if (!first) {
+// out.append("; ");
+// }
+// out.append("ENUM" + counter + " = {");
+// Iterator<String> it2 = e.modelvalues.iterator();
+// while (it2.hasNext()) {
+// out.append(it2.next());
+// if (it2.hasNext()) {
+// out.append(", ");
+// }
+// }
+// if (e.hasNoVal()) {
+// out.append(", noVal" + counter);
+// }
+// out.append("}");
+// printed.add(e);
+// counter++;
+// first = false;
}
}
- if (operatorModelvalues != null && operatorModelvalues.size() > 0) {
- for (int i = 0; i < operatorModelvalues.size(); i++) {
- OpDefNode def = operatorModelvalues.get(i);
- TLAType type = (TLAType) def.getToolObject(TYPE_ID);
- EnumType e = null;
- if (type instanceof SetType) {
- if (((SetType) type).getSubType() instanceof EnumType) {
- e = (EnumType) ((SetType) type).getSubType();
- } else
- continue;
-
- } else if ((type instanceof EnumType)) {
- e = (EnumType) type;
- } else
- continue;
-
- if (!printed.contains(e)) {
- e.id = counter;
- if (!first) {
- out.append("; ");
- }
- out.append("ENUM" + counter + " = {");
- Iterator<String> it2 = e.modelvalues.iterator();
- while (it2.hasNext()) {
- out.append(it2.next());
- if (it2.hasNext()) {
- out.append(", ");
- }
- }
- if (e.hasNoVal()) {
- out.append(", noVal" + counter);
- }
- out.append("}");
- printed.add(e);
- counter++;
- first = false;
- }
-
- }
-
- }
+// if (operatorModelvalues != null && operatorModelvalues.size() > 0) {
+// for (int i = 0; i < operatorModelvalues.size(); i++) {
+// OpDefNode def = operatorModelvalues.get(i);
+// TLAType type = (TLAType) def.getToolObject(TYPE_ID);
+// EnumType e = null;
+// if (type instanceof SetType) {
+// if (((SetType) type).getSubType() instanceof EnumType) {
+// e = (EnumType) ((SetType) type).getSubType();
+// } else
+// continue;
+//
+// } else if ((type instanceof EnumType)) {
+// e = (EnumType) type;
+// } else
+// continue;
+//
+// if (!printed.contains(e)) {
+// e.id = counter;
+// if (!first) {
+// out.append("; ");
+// }
+// out.append("ENUM" + counter + " = {");
+// Iterator<String> it2 = e.modelvalues.iterator();
+// while (it2.hasNext()) {
+// out.append(it2.next());
+// if (it2.hasNext()) {
+// out.append(", ");
+// }
+// }
+// if (e.hasNoVal()) {
+// out.append(", noVal" + counter);
+// }
+// out.append("}");
+// printed.add(e);
+// counter++;
+// first = false;
+// }
+//
+// }
+//
+// }
out.append("\n");
return out;
diff --git a/src/main/java/de/tla2b/translation/Tla2BTranslator.java b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
index 8e67de3e736bb02be21cb972aed8c4082682238c..7ec593ee29303a4629a23d696613764c1b222999 100644
--- a/src/main/java/de/tla2b/translation/Tla2BTranslator.java
+++ b/src/main/java/de/tla2b/translation/Tla2BTranslator.java
@@ -122,16 +122,16 @@ public class Tla2BTranslator implements TranslationGlobals {
typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
typechecker.start();
- specAnalyser.evalIfThenElse();
+ //specAnalyser.evalIfThenElse();
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
- BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
- specAnalyser);
+// BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
+// specAnalyser);
// BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
// specAnalyser);
- return p.start();
+ return null;
}
public static ModuleNode parseModule(String moduleName)
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 49df90e5a8c95cbfb7bd1e65f302847d6306f71f..c885712c9baf614e488f8250f518936f26e9d2b2 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -2,7 +2,6 @@ package de.tla2bAst;
import java.util.ArrayList;
import java.util.Arrays;
-import java.util.Collection;
import java.util.HashSet;
import java.util.Hashtable;
import java.util.Iterator;
@@ -249,6 +248,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
ArrayList<PSet> sets = new ArrayList<PSet>();
for (int i = 0; i < printed.size(); i++) {
AEnumeratedSetSet eSet = new AEnumeratedSetSet();
+ printed.get(i).id = i + 1;
eSet.setIdentifier(createTIdentifierLiteral("ENUM" + (i + 1)));
List<PExpression> list = new ArrayList<PExpression>();
for (Iterator<String> iterator = printed.get(i).modelvalues
@@ -503,9 +503,9 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
constantsList.add(id);
}
- for (RecursiveFunktion recFunc : specAnalyser.getRecursiveFunctions()) {
+ for (OpDefNode recFunc : specAnalyser.getRecursiveFunctions()) {
AIdentifierExpression id = new AIdentifierExpression(
- createTIdentifierLiteral(getName(recFunc.getOpDefNode())));
+ createTIdentifierLiteral(getName(recFunc)));
constantsList.add(id);
}
@@ -530,7 +530,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
propertiesList.addAll(evalRecursiveDefinitions());
- //propertiesList.addAll(evalRecursiveFunctions());
+ propertiesList.addAll(evalRecursiveFunctions());
for (OpDeclNode con : bConstants) {
if (conEval != null
@@ -612,32 +612,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private List<PPredicate> evalRecursiveFunctions() {
List<PPredicate> propertiesList = new ArrayList<PPredicate>();
- for (RecursiveFunktion recDef : specAnalyser.getRecursiveFunctions()) {
-
-
- OpDefNode def = recDef.getOpDefNode();
- FormalParamNode[] params = def.getParams();
- ArrayList<PExpression> paramList1 = new ArrayList<PExpression>();
- ArrayList<PPredicate> typeList = new ArrayList<PPredicate>();
- // ArrayList<PExpression> paramList2 = new ArrayList<PExpression>();
- for (FormalParamNode p : params) {
- paramList1.add(createIdentifierNode(p));
- // paramList2.add(createIdentifierNode(p.getName().toString()));
- TLAType paramType = (TLAType) p.getToolObject(TYPE_ID);
- // System.out.println(paramType);
- AEqualPredicate equal = new AEqualPredicate(
- createIdentifierNode(p), paramType.getBNode());
- typeList.add(equal);
- }
- ALambdaExpression lambda1 = new ALambdaExpression();
- lambda1.setIdentifiers(paramList1);
- lambda1.setPredicate(createConjunction(typeList));
- lambda1.setExpression(visitExprNodeExpression(def.getBody()));
+ for (OpDefNode def : specAnalyser.getRecursiveFunctions()) {
AEqualPredicate equals = new AEqualPredicate(
- createIdentifierNode(def), lambda1);
+ createIdentifierNode(def),
+ visitExprNodeExpression(def.getBody()));
propertiesList.add(equals);
-
-
}
return propertiesList;
@@ -810,14 +789,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
private PPredicate visitOpApplNodePredicate(OpApplNode n) {
switch (n.getOperator().getKind()) {
- case ConstantDeclKind: {
- return new AEqualPredicate(createIdentifierNode(n.getOperator()),
- new ABooleanTrueExpression());
- }
- case VariableDeclKind: {
+ case VariableDeclKind:
+ case ConstantDeclKind:
+ case FormalParamKind: {
return new AEqualPredicate(createIdentifierNode(n.getOperator()),
new ABooleanTrueExpression());
-
}
case BuiltInKind:
return visitBuiltInKindPredicate(n);
@@ -878,6 +854,11 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
for (int i = 0; i < n.getArgs().length; i++) {
params.add(visitExprOrOpArgNodeExpression(n.getArgs()[i]));
}
+ if (specAnalyser.getRecursiveFunctions().contains(def)) {
+ return new AEqualPredicate(createIdentifierNode(def),
+ new ABooleanTrueExpression());
+ }
+
if (predicateVsExpression.getDefinitionType(def) == DefinitionType.EXPRESSION) {
ADefinitionExpression defCall = new ADefinitionExpression();
defCall.setDefLiteral(new TIdentifierLiteral(getName(def)));
@@ -907,6 +888,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return visitBBuitInsExpression(n);
}
+ if (specAnalyser.getRecursiveFunctions().contains(def)) {
+ return createIdentifierNode(def);
+ }
+
if (allTLADefinitions.contains(def)) {
List<PExpression> params = new ArrayList<PExpression>();
for (int i = 0; i < n.getArgs().length; i++) {
@@ -1341,15 +1326,42 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
List<PExpression> idList = new ArrayList<PExpression>();
List<PPredicate> predList = new ArrayList<PPredicate>();
- for (int i = 0; i < bounds.length; i++) {
- FormalParamNode p = params[i][0];
- AMemberPredicate member = new AMemberPredicate();
- member.setLeft(createIdentifierNode(p));
- ExprNode in = n.getBdedQuantBounds()[i];
- member.setRight(visitExprNodeExpression(in));
- predList.add(member);
- idList.add(createIdentifierNode(p));
+
+ for (int i = 0; i < params.length; i++) {
+ if (n.isBdedQuantATuple()[i]) {
+ List<PExpression> list = new ArrayList<PExpression>();
+ for (FormalParamNode formalParam : params[i]) {
+ list.add(createIdentifierNode(formalParam));
+ idList.add(createIdentifierNode(formalParam));
+ }
+ ACoupleExpression couple = new ACoupleExpression(list);
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(couple);
+ ExprNode in = n.getBdedQuantBounds()[i];
+ member.setRight(visitExprNodeExpression(in));
+ predList.add(member);
+ } else {
+ for (FormalParamNode formalParam : params[i]) {
+ AMemberPredicate member = new AMemberPredicate();
+ member.setLeft(createIdentifierNode(formalParam));
+ ExprNode in = n.getBdedQuantBounds()[i];
+ member.setRight(visitExprNodeExpression(in));
+ predList.add(member);
+ idList.add(createIdentifierNode(formalParam));
+ }
+ }
+
}
+ // for (int i = 0; i < bounds.length; i++) {
+ //
+ // FormalParamNode p = params[i][0];
+ // AMemberPredicate member = new AMemberPredicate();
+ // member.setLeft(createIdentifierNode(p));
+ // ExprNode in = n.getBdedQuantBounds()[i];
+ // member.setRight(visitExprNodeExpression(in));
+ // predList.add(member);
+ // idList.add(createIdentifierNode(p));
+ // }
final String nameOfTempVariable = "t_";
AEqualPredicate equals = new AEqualPredicate();
equals.setLeft(createIdentifierNode(nameOfTempVariable));
@@ -1629,6 +1641,21 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals,
return createBoundedChoose(n);
}
+ case OPCODE_bf: { // \A x \in S : P
+ FormalParamNode[][] params = n.getBdedQuantSymbolLists();
+ ArrayList<PExpression> list = new ArrayList<PExpression>();
+ for (int i = 0; i < params.length; i++) {
+ for (int j = 0; j < params[i].length; j++) {
+ list.add(createIdentifierNode(params[i][j]));
+ }
+ }
+ AImplicationPredicate implication = new AImplicationPredicate();
+ implication.setLeft(visitBounded(n));
+ implication.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
+ return new AConvertBoolExpression(new AForallPredicate(list,
+ implication));
+ }
+
}
System.out.println(n.getOperator().getName());
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 4d62bcc7f348fa5728226c7955498e1844c58791..199fb4812b2574845785a178402e3a47254b14dd 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -108,7 +108,7 @@ public class Translator implements TranslationGlobals {
parse();
}
- public ModuleNode parseModule2()
+ public ModuleNode parseModule()
throws de.tla2b.exceptions.FrontEndException {
String fileName = moduleFile.getName();
ToolIO.setUserDir(moduleFile.getParent());
@@ -158,7 +158,7 @@ public class Translator implements TranslationGlobals {
}
private void parse() throws FrontEndException {
- moduleNode = parseModule2();
+ moduleNode = parseModule();
modelConfig = null;
if (configFile != null) {
@@ -193,25 +193,21 @@ public class Translator implements TranslationGlobals {
} else {
specAnalyser = new SpecAnalyser(moduleNode);
}
-
specAnalyser.start();
-
TypeChecker typechecker = new TypeChecker(moduleNode, conEval,
specAnalyser);
typechecker.start();
-
- specAnalyser.evalIfThenElse();
+ //specAnalyser.evalIfThenElse();
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
- BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
- specAnalyser);
- bMachineString = p.start().toString();
+// BMachinePrinter p = new BMachinePrinter(moduleNode, conEval,
+// specAnalyser);
+// bMachineString = p.start().toString();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
moduleNode, specAnalyser);
-
BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
BAstCreator bAstCreator = new BAstCreator(moduleNode, conEval,
specAnalyser, usedExternalFunctions, predicateVsExpression, bMacroHandler);
@@ -305,5 +301,9 @@ public class Translator implements TranslationGlobals {
public String getBMachineString() {
return bMachineString;
}
+
+ public ModuleNode getModuleNode(){
+ return moduleNode;
+ }
}
diff --git a/src/test/java/de/tla2b/examples/MCTest.java b/src/test/java/de/tla2b/examples/MCTest.java
index c70a1d5aa0871f453dc6874a8a3b03d5d8bb6242..ee9ee41ce137284827b2e4e2cabb0274a610ca51 100644
--- a/src/test/java/de/tla2b/examples/MCTest.java
+++ b/src/test/java/de/tla2b/examples/MCTest.java
@@ -112,4 +112,16 @@ public class MCTest {
String file = "src/test/resources/examples/SumAndProduct/SumAndProductConstraint.tla";
runModule(file);
}
+
+ @Test
+ public void testuf50_02() throws Exception {
+ String file = "src/test/resources/examples/uf50_02/uf50_02.tla";
+ runModule(file);
+ }
+
+ @Test
+ public void testRecursiveFunction() throws Exception {
+ String file = "src/test/resources/examples/RecursiveFunction/RecursiveFunction.tla";
+ runModule(file);
+ }
}
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index 9d4044acf558c3d2c15dfa7f2697513c3571b481..164a417a422931f8d2ac2a9c4bfdcaddfca5908f 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -17,10 +17,8 @@ public class LogicOperatorsTest {
+ "ASSUME k = (2 # 1)\n"
+ "=================================";
- final String expected = "MACHINE Testing\n"
- + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES k : BOOL & k = bool(2 /= 1)\n"
- + "END";
+ final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
+ + "PROPERTIES k : BOOL & k = bool(2 /= 1)\n" + "END";
compare(expected, module);
}
@@ -139,7 +137,6 @@ public class LogicOperatorsTest {
compare(expected, module);
}
-
@Test
public void testQuantifier() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
index df0cdc6df06653ed79002ec7fa0c9837639d7b74..b2f3c81ab0b9de5389256b8614745f4730e8e0ab 100644
--- a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java
@@ -6,7 +6,7 @@ import org.junit.Ignore;
import org.junit.Test;
public class RecursiveFunctionTest {
-
+
@Ignore
@Test
public void testRecursiveDefinition() throws Exception {
@@ -17,10 +17,41 @@ public class RecursiveFunctionTest {
+ "=================================";
final String expected = "MACHINE Testing\n" + "ABSTRACT_CONSTANTS k\n"
- + "PROPERTIES "
- + " k : BOOL +-> INTEGER "
+ + "PROPERTIES " + " k : BOOL +-> INTEGER "
+ "& k = k <+ {TRUE |-> 0, FALSE |-> 0}" + "END";
compare(expected, module);
-
+
+ }
+
+ @Test
+ public void testFactorial() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "fac[x \\in Nat] == IF x = 1 THEN 1 ELSE x * fac[x-1]\n"
+ + "ASSUME fac[3] = 6 \n" + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "ABSTRACT_CONSTANTS fac\n"
+ + "PROPERTIES "
+ + "fac = %(x).(x : NATURAL | (%(t_).(t_ = 0 & x = 1 | 1) \\/ %(t_).(t_ = 0 & not(x = 1) | x * fac((x - 1))))(0)) & fac(3) = 6 \n"
+ + "END";
+ compare(expected, module);
+
+ }
+
+ @Test
+ public void testFactorial2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "fac[x \\in Nat] == 5 + IF x = 1 THEN 1 ELSE x * fac[x-1]\n"
+ + "ASSUME fac[3] = 56 \n" + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "ABSTRACT_CONSTANTS fac\n"
+ + "PROPERTIES "
+ + "fac = %(x).(x : NATURAL | 5 + (%(t_).(t_ = 0 & x = 1 | 1) \\/ %(t_).(t_ = 0 & not(x = 1) | x * fac((x - 1))))(0)) & fac(3) = 56 \n"
+ + "END";
+ compare(expected, module);
+
}
}
diff --git a/src/test/java/de/tla2b/prettyprintb/SetsTest.java b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
index 3aa124e52abb19eb1d797a47ed239a785befa289..e1c16a71a57c0e5c6d1d2a1a6a18fcc67215c966 100644
--- a/src/test/java/de/tla2b/prettyprintb/SetsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/SetsTest.java
@@ -196,4 +196,17 @@ public class SetsTest {
+ "PROPERTIES {x|x : {1, 2, 3} & (x : {1} or x : {2})} = {1, 2} \n" + "END";
compare(expected, module);
}
+
+ @Test
+ public void testConstructor4() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "ASSUME {1} = {x : <<x, y>> \\in {1} \\X {2}} \n"
+ + "=================================";
+ final String expected = "MACHINE Testing\n"
+ + "PROPERTIES {1} = {t_ | #(x,y).((x,y) : {1} * {2} & t_ = x)} \n"
+ + "END";
+ compare(expected, module);
+ }
+
}
diff --git a/src/test/java/de/tla2b/typechecking/InstanceTest.java b/src/test/java/de/tla2b/typechecking/InstanceTest.java
index 44241dcd1326a44bf7b79bd3c5adcf3bd9b41bfb..329a772f0855ba85b5c7e53c40172c9ce00f25bb 100644
--- a/src/test/java/de/tla2b/typechecking/InstanceTest.java
+++ b/src/test/java/de/tla2b/typechecking/InstanceTest.java
@@ -49,8 +49,7 @@ public class InstanceTest {
@Test
public void TestInstanceValue() throws Exception {
- TestTypeChecker t = TestUtil.typeCheck(path + "InstanceValue.tla",
- "InstanceValue.cfg");
+ TestTypeChecker t = TestUtil.typeCheck(path + "InstanceValue.tla");
assertEquals("INTEGER", t.getConstantType("c2"));
assertEquals("INTEGER", t.getConstantType("val2"));
}
diff --git a/src/test/java/de/tla2b/util/TestTypeChecker.java b/src/test/java/de/tla2b/util/TestTypeChecker.java
index c80cb23e45c15c653d2f8024950b8439f3e7be85..cbe0d5e9eddb70bd3d11c66a49be814e166a92d7 100644
--- a/src/test/java/de/tla2b/util/TestTypeChecker.java
+++ b/src/test/java/de/tla2b/util/TestTypeChecker.java
@@ -11,7 +11,7 @@ import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.translation.Tla2BTranslator;
import de.tla2b.types.TLAType;
-
+import de.tla2bAst.Translator;
import tla2sany.semantic.FormalParamNode;
import tla2sany.semantic.ModuleNode;
import tla2sany.semantic.OpDeclNode;
@@ -33,17 +33,15 @@ public class TestTypeChecker implements TranslationGlobals {
public void startTest(String moduleString, String configString)
throws FrontEndException, TLA2BException {
- Tla2BTranslator translator = new Tla2BTranslator();
- translator.startTest(moduleString, configString);
+ Translator translator = new Translator(moduleString, configString);
translator.translate();
moduleNode = translator.getModuleNode();
init();
}
- public void start(String moduleFileName, String configFileName)
+ public void start(String moduleFileName)
throws FrontEndException, TLA2BException {
- Tla2BTranslator translator = new Tla2BTranslator();
- translator.start(moduleFileName, configFileName);
+ Translator translator = new Translator(moduleFileName);
translator.translate();
moduleNode = translator.getModuleNode();
init();
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index ed216ee08e6f51deea8f6e34181fb24027049238..f7146256f376753125e04a429e303c8700fd5302 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -115,6 +115,10 @@ public class TestUtil {
Translator trans = new Translator(tlaModule, config);
Start resultNode = trans.translate();
+ ASTPrettyPrinter aP = new ASTPrettyPrinter();
+ resultNode.apply(aP);
+ System.out.println(aP.getResultString());
+
//BParser.printASTasProlog(System.out, new BParser(), new File("./test.mch"), resultNode, false, true, null);
String result = getTreeAsString(resultNode);
@@ -197,20 +201,10 @@ public class TestUtil {
ToolIO.reset();
moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
TestTypeChecker testTypeChecker = new TestTypeChecker();
- testTypeChecker.start(moduleFileName, null);
+ testTypeChecker.start(moduleFileName);
return testTypeChecker;
}
- public static TestTypeChecker typeCheck(String moduleFileName, String configFileName) throws FrontEndException, TLA2BException{
- ToolIO.setMode(ToolIO.TOOL);
- ToolIO.reset();
- moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
- configFileName = configFileName.replace('/', FileUtil.separatorChar);
- TestTypeChecker testTypeChecker = new TestTypeChecker();
- testTypeChecker.start(moduleFileName, configFileName);
- return testTypeChecker;
- }
-
public static String fileToString(String fileName) throws IOException {
StringBuilder res = new StringBuilder();
diff --git a/src/test/resources/examples/Relations.tla b/src/test/resources/examples/Relations.tla
deleted file mode 100644
index a9a1bc1e0f5c3c8fc88150450a8c35d948f19437..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/Relations.tla
+++ /dev/null
@@ -1,66 +0,0 @@
------------------------------ MODULE Relations -----------------------------
-
-EXTENDS TLC, Sequences, Naturals, FiniteSets, Integers
-
-domain(r) == {x[1]: x \in r}
-range(r) == {x[2]: x \in r}
-id(S) == {<<x,x>>: x \in S}
-set_of_relations(x,y) == SUBSET (x \times y)
-domain_restriction(S, r) == {x \in r: x[1] \in S}
-domain_substraction(S, r) == {x \in r: x[1] \notin S}
-range_restriction(S, r) == {x \in r: x[2] \in S}
-range_substraction(S, r) == {x \in r: x[2] \notin S}
-
-rel_inverse(r) == {<<x[2],x[1]>>: x\in r}
-relational_image(r, S) =={y[2] :y \in {x \in r: x[1] \in S}}
-relational_overriding(r, r2) == {x \in r: x[1] \notin domain(r2)} \cup r2
-
-
-direct_product(r1, r2) == {<<x, u>> \in (domain(r1)\cup domain(r2)) \times (range(r1) \times range(r2)):
- u[1] \in relational_image(r1, {x}) /\ u[2] \in relational_image(r2,{x})}
-direct_product2(r1, r2) == {u \in (domain(r1)\cup domain(r2)) \times (range(r1) \times range(r2)):
- <<u[1],u[2][1]>> \in r1 /\ <<u[1],u[2][2]>> \in r2}
-
-relational_composition(r1, r2) == {<<u[1][1],u[2][2]>> : u \in
- {x \in range_restriction(domain(r2),r1) \times domain_restriction(range(r1),r2): x[1][2] = x[2][1]}
- }
-
-prj1(E, F) == {u \in E \times F \times E: u[1] = u[3]}
-prj2(E, F) == {u \in E \times F \times F: u[2] = u[3]}
-
-
-RECURSIVE iterate(_,_)
-iterate(r, n) == CASE n = 0 -> id(domain(r)\cup range(r))
- [] n = 1 -> r
- [] OTHER -> iterate(relational_composition(r,r), n-1)
-
-RECURSIVE closure1(_)
-closure1(R) == IF relational_composition(R,R) \R # {}
- THEN R \cup closure1(relational_composition(R,R))
- ELSE R
-
-closure(R) == closure1( R \cup {<<x[1],x[1]>>: x \in R} \cup {<<x[2],x[2]>>: x \in R})
-
-relational_call(r, x) == (CHOOSE y \in r: y[1] = x)[2]
-
-
-is_partial_func(f) == \A x \in domain(f): Cardinality(relational_image(f, {x})) <= 1
-is_partial_func2(f, S, S2) == /\ \A x \in f: x[1] \in S /\ x[2] \in S2 /\ relational_image(f, {x[1]}) = {x[2]}
-
-partial_func(S, S2) == {x \in (SUBSET (S \times S2)): is_partial_func(x)}
-
-is_func(f) == \A x \in domain(f): Cardinality(relational_image(f, {x})) < 2
-total_func(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x) /\ domain(x)= S}
-
-is_total_func(f, S, S2) == domain(f) = S /\ \A x \in f: x[1] \in S /\ x[2] \in S2 /\ relational_image(f, {x[1]}) = {x[2]}
-
-is_injectiv_func(f) == \A x \in range(f): Cardinality(relational_image(rel_inverse(f), {x})) <= 1
-total_injection(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x) /\ domain(x)= S /\ is_injectiv_func(x) }
-partial_injection(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x) /\ is_injectiv_func(x) }
-
-total_surjection(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x)/\ domain(x)= S /\ S2 = range(x)}
-partial_surjection(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x)/\ S2 = range(x)}
-
-total_bijection(S, S2) == {x \in (SUBSET (S \times S2)): is_func(x) /\ domain(x) = S /\ is_injectiv_func(x) /\ S2 = range(x)}
-
-=============================================================================
\ No newline at end of file
diff --git a/src/test/resources/examples/SecCtx.cfg b/src/test/resources/examples/SecCtx.cfg
deleted file mode 100644
index d9bdb0b9b1707d86c7a668bc84dfa3d5759b8f0e..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/SecCtx.cfg
+++ /dev/null
@@ -1,8 +0,0 @@
-INIT SecCtx_Init
-NEXT SecCtx_Next
-INVARIANT Inv
-CONSTANTS
-usr_lst_cnt = 2
-REG_USR = {0,1}
-NAT = {0,1,2,3}
-INT = {0,1,2,3}
\ No newline at end of file
diff --git a/src/test/resources/examples/SecCtx.tla b/src/test/resources/examples/SecCtx.tla
deleted file mode 100644
index a31684ddcf69f96b1eaa4388fa8e5b4e8ae223cf..0000000000000000000000000000000000000000
--- a/src/test/resources/examples/SecCtx.tla
+++ /dev/null
@@ -1,475 +0,0 @@
-------------------------------- MODULE SecCtx -------------------------------
-EXTENDS Naturals, Integers, Relations
-CONSTANTS usr_lst_cnt, REG_USR, INT, NAT
-ASSUME usr_lst_cnt \in Nat\{0} /\ REG_USR = 0..(usr_lst_cnt-1)
-
-min(S) == CHOOSE x \in S : \A i \in S: x \leq i
-
-VARIABLES
- flg_comm_active, (* communicating *)
- flg_got_cli_nonce, (* Client Nonce received *)
- flg_sent_serv_nonce, (* Server Nonce sent *)
- flg_sent_cert, (* Server certificate sent *)
- flg_got_premaster, (* premaster secret received from client *)
- flg_set_cmn_key, (* session common key set *)
- flg_done_hs_verify, (* Data for verifying a Handshake message checked *)
- flg_sent_hs_verify, (* Data for verifying a Handshake message sent *)
- flg_cipher_on, (* Applied encryption to communication data *)
-
- flg_allow_user_auth, (* the propriety user authenticating user *)
- flg_done_user_auth, (* user authenticated flag *)
- flg_allow_user_data, (* the propriety sending and receiving user data flag *)
-
- flg_tx_msg_encoded, (* encryption of sending data flag *)
- flg_tx_add_mac, (* Given MAC of sending data flag *)
- flg_allow_send_data, (* Permission of sending TCP data flag*)
-
- flg_rx_msg_decoded, (* encryption of receiviing data flag *)
- flg_rx_chk_mac, (* Given MAC of receiviing data flag *)
- flg_allow_recv_data, (* Permission of giving application software received data flag*)
-
- auth_fail_cnt, (* consecutive unsuccessful authentication attempts for each user *)
- recent_auth_tim (* previous time of authentication attempts for each user for each user *)
-
-Inv == (* Definition of type *)
- (* -------------------------------------------------------- *)
- flg_comm_active \in BOOLEAN /\
- flg_got_cli_nonce \in BOOLEAN /\
- flg_sent_serv_nonce \in BOOLEAN /\
- flg_sent_cert \in BOOLEAN /\
- flg_got_premaster \in BOOLEAN /\
- flg_set_cmn_key \in BOOLEAN /\
- flg_done_hs_verify \in BOOLEAN /\
- flg_sent_hs_verify \in BOOLEAN /\
- flg_cipher_on \in BOOLEAN /\
-
- flg_allow_user_auth \in BOOLEAN /\
- flg_done_user_auth \in BOOLEAN /\
- flg_allow_user_data \in BOOLEAN /\
-
- flg_tx_msg_encoded \in BOOLEAN /\
- flg_tx_add_mac \in BOOLEAN /\
- flg_allow_send_data \in BOOLEAN /\
-
- flg_rx_msg_decoded \in BOOLEAN /\
- flg_rx_chk_mac \in BOOLEAN /\
- flg_allow_recv_data \in BOOLEAN /\
-
- is_total_func(auth_fail_cnt, REG_USR, NAT) /\ (* auth_fail_cnt : REG_USR +-> NAT & dom(auth_fail_cnt)=REG_USR &*)
- is_total_func(recent_auth_tim, REG_USR, INT) /\ (*recent_auth_tim : REG_USR +-> INT & dom(recent_auth_tim)=REG_USR &*)
-
- (flg_sent_serv_nonce=TRUE => flg_got_cli_nonce=TRUE) /\
- (flg_sent_cert=TRUE => flg_sent_serv_nonce=TRUE) /\
- (flg_got_premaster=TRUE => flg_sent_cert=TRUE) /\
- (flg_sent_hs_verify=TRUE => flg_got_premaster=TRUE) /\
- (flg_allow_user_auth = TRUE
- => (flg_sent_cert = TRUE) /\ (flg_got_premaster=TRUE) /\ (flg_sent_hs_verify=TRUE))
-
- /\ (flg_allow_user_data = TRUE
- => (flg_sent_cert = TRUE) /\ (flg_got_premaster=TRUE) /\ (flg_sent_hs_verify=TRUE))
-
- /\
- (* Encryption of user data：Prevent eavesdropping *)
- ( flg_cipher_on=TRUE => flg_set_cmn_key=TRUE) /\
- ( flg_allow_user_auth=TRUE => flg_cipher_on=TRUE) /\
- ( flg_done_user_auth=TRUE => flg_allow_user_auth=TRUE) /\
- ( flg_allow_send_data=TRUE => (flg_allow_user_data=TRUE)/\(flg_tx_msg_encoded=TRUE) ) /\
- ( flg_allow_recv_data=TRUE => (flg_allow_user_data=TRUE)/\(flg_rx_msg_decoded=TRUE) ) /\
-
-
- (* Make the unique common key for every session：Prevent replying *)
- ( flg_allow_user_auth=TRUE => flg_done_hs_verify=TRUE ) /\
- ( flg_allow_user_auth=TRUE => flg_sent_hs_verify=TRUE ) /\
- ( flg_cipher_on=TRUE => flg_got_cli_nonce=TRUE ) /\
- ( flg_cipher_on=TRUE => flg_sent_serv_nonce=TRUE ) /\
- ( flg_comm_active=FALSE => flg_set_cmn_key=FALSE) /\
-
- (* Make hash：Prevent Prevent falsifying(contain adding messages,
- deleting messages and replacing an order of a message ) and replying *)
- ( flg_allow_send_data=TRUE => (flg_allow_user_data=TRUE)/\(flg_tx_add_mac=TRUE) ) /\
- ( flg_allow_recv_data=TRUE => (flg_allow_user_data=TRUE)/\(flg_rx_chk_mac=TRUE) ) /\
-
- (* Authenticate User：Prevent masquerading as an user *)
- ( flg_allow_user_auth = TRUE => flg_cipher_on = TRUE ) /\
- ( flg_allow_user_data = TRUE => flg_done_user_auth = TRUE )
-
-
-SecCtx_Init ==
- flg_comm_active = FALSE /\
- flg_got_cli_nonce = FALSE /\
- flg_sent_serv_nonce = FALSE /\
- flg_sent_cert = FALSE /\
- flg_got_premaster = FALSE /\
- flg_set_cmn_key = FALSE /\
- flg_done_hs_verify = FALSE /\
- flg_sent_hs_verify = FALSE /\
- flg_cipher_on = FALSE /\
- flg_allow_user_auth = FALSE /\
- flg_done_user_auth = FALSE /\
- flg_allow_user_data = FALSE /\
-
- flg_tx_msg_encoded = FALSE /\
- flg_tx_add_mac = FALSE /\
- flg_allow_send_data = FALSE /\
-
- flg_rx_msg_decoded = FALSE /\
- flg_rx_chk_mac = FALSE /\
- flg_allow_recv_data = FALSE /\
-
- auth_fail_cnt = REG_USR \times {0} /\
- recent_auth_tim = (REG_USR \times {-1})
-
-
-
- (* Set flag operations *)
-SetFlgCommActive ==
- /\ flg_comm_active = FALSE
- /\ flg_comm_active' = TRUE
- /\ UNCHANGED << flg_got_cli_nonce,flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key, flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth, flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded, flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim >>
-
-SetFlgGotCliNonce ==
- /\ flg_got_cli_nonce' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-SetFlgSentServNonce ==
- /\ flg_got_cli_nonce = TRUE
- /\ flg_sent_serv_nonce' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-SetFlgSentCert ==
- /\ flg_sent_serv_nonce = TRUE
- /\ flg_sent_cert' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-SetFlgGotPremaster ==
- /\ flg_sent_cert = TRUE
- /\ flg_got_premaster' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgCmnKey ==
- /\ (flg_comm_active = TRUE)
- /\ (flg_got_premaster = TRUE)
- /\ (flg_got_cli_nonce = TRUE)
- /\ (flg_sent_serv_nonce = TRUE)
- /\ flg_set_cmn_key' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgCipherOn ==
- /\ (flg_got_premaster = TRUE)
- /\ (flg_got_cli_nonce = TRUE)
- /\ (flg_sent_serv_nonce = TRUE)
- /\ (flg_set_cmn_key = TRUE)
- /\ flg_cipher_on' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgDoneHsVerify ==
- /\ flg_done_hs_verify' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-
-SetFlgSentHsVerify ==
- /\ flg_got_premaster = TRUE
- /\ flg_sent_hs_verify' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-
-SetFlgAllowUserAuth ==
- /\ (flg_cipher_on = TRUE)
- /\ (flg_done_hs_verify = TRUE)
- /\ (flg_sent_hs_verify = TRUE)
- /\ flg_allow_user_auth' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgDoneUserAuth ==
- /\ flg_allow_user_auth = TRUE
- /\ flg_done_user_auth' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetSuccessUserAuth(usr, tim) ==
- /\ usr \in INT /\ usr \in REG_USR /\ tim \in INT
- /\ flg_allow_user_auth = TRUE
-
- /\ flg_done_user_auth' = TRUE
- /\ auth_fail_cnt'= relational_overriding(auth_fail_cnt, {<<usr,0>>})
- /\ recent_auth_tim' = relational_overriding(recent_auth_tim, {<<usr, tim>>})
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data>>
-
-SetFailUserAuth(usr, tim) ==
- /\ usr \in INT /\ usr \in REG_USR /\ tim \in INT
- /\ flg_done_user_auth' = FALSE
- /\ flg_allow_user_data' = FALSE
- /\ flg_allow_send_data' = FALSE
- /\ flg_allow_recv_data' = FALSE
- /\ auth_fail_cnt' = relational_overriding(auth_fail_cnt, {<<usr,min({relational_call(auth_fail_cnt,usr)+1, 3})>>})
- /\ recent_auth_tim' = relational_overriding(recent_auth_tim, {<<usr, tim>>})
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth, flg_tx_msg_encoded,flg_tx_add_mac,flg_rx_msg_decoded,flg_rx_chk_mac>>
-
- SetFlgAllowUserData ==
- /\ (flg_sent_cert = TRUE)
- /\ (flg_got_premaster=TRUE)
- /\ (flg_sent_hs_verify = TRUE)
- /\ (flg_cipher_on = TRUE)
- /\ (flg_done_user_auth = TRUE)
- /\ flg_allow_user_data' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-SetFlgTxMsgEncoded ==
- /\ flg_tx_msg_encoded' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgTxAddMac ==
- /\ flg_tx_add_mac' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgAllowSendData ==
- /\ (flg_allow_user_data=TRUE)
- /\ (flg_tx_msg_encoded = TRUE)
- /\ (flg_tx_add_mac = TRUE)
- /\ flg_allow_send_data' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgRxMsgDecoded ==
- /\ flg_rx_msg_decoded' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetFlgRxChkMac ==
- /\ flg_rx_chk_mac' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-
-SetFlgAllowRecvData ==
- /\ flg_cipher_on = TRUE
- /\ (flg_allow_user_data = TRUE)
- /\ (flg_rx_msg_decoded = TRUE)
- /\ (flg_rx_chk_mac = TRUE)
- /\ flg_allow_recv_data' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,auth_fail_cnt,recent_auth_tim>>
-
- (* Complete Handshake *)
-SetFlgsHndshkCompleteSts ==
- flg_comm_active' = TRUE /\
- flg_got_cli_nonce' = TRUE /\
- flg_sent_serv_nonce' = TRUE /\
- flg_sent_cert' = TRUE /\
- flg_got_premaster' = TRUE /\
- flg_set_cmn_key' = TRUE /\
- flg_done_hs_verify' = TRUE /\
- flg_sent_hs_verify' = TRUE /\
- flg_cipher_on' = TRUE /\
- flg_allow_user_auth' = TRUE
- /\ UNCHANGED <<flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
- (* Reset Handshake Status *)
-ResetFlgsHndshkCompleteSts ==
- /\ flg_allow_user_data = FALSE
-
- /\ flg_comm_active' = FALSE /\
- flg_got_cli_nonce' = FALSE /\
- flg_sent_serv_nonce' = FALSE /\
- flg_sent_cert' = FALSE /\
- flg_got_premaster' = FALSE /\
- flg_set_cmn_key' = FALSE /\
- flg_done_hs_verify' = FALSE /\
- flg_sent_hs_verify' = FALSE /\
- flg_cipher_on' = FALSE /\
- flg_allow_user_auth' = FALSE /\
- flg_done_user_auth' =FALSE
- /\ UNCHANGED <<flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
- (* Complete user authentication *)
-SetFlgsAuthCompleteSts ==
- /\ flg_allow_user_auth = TRUE
- /\
- flg_done_user_auth' = TRUE /\
- flg_allow_user_data' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
- (* Reset user authentication status *)
-ResetFlgsAuthCompleteSts ==
- /\
- flg_done_user_auth' = FALSE /\
- flg_allow_user_data' = FALSE /\
-
- flg_allow_send_data' = FALSE /\
- flg_allow_recv_data' = FALSE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth, flg_tx_msg_encoded,flg_tx_add_mac,flg_rx_msg_decoded,flg_rx_chk_mac,auth_fail_cnt,recent_auth_tim>>
-
-
- (* Complete https_acp successfully *)
-SetFlgsAcpCompleteSts ==
- /\
- flg_comm_active' = TRUE /\
- flg_got_cli_nonce' = TRUE /\
- flg_sent_serv_nonce' = TRUE /\
- flg_sent_cert' = TRUE /\
- flg_got_premaster' = TRUE /\
- flg_set_cmn_key' = TRUE /\
- flg_done_hs_verify' = TRUE /\
- flg_sent_hs_verify' = TRUE /\
- flg_cipher_on' = TRUE /\
- flg_allow_user_auth' = TRUE /\
- flg_done_user_auth' = TRUE /\
- flg_allow_user_data' = TRUE
- /\ UNCHANGED <<flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
- (* Reset https_acp status *)
-ResetFlgsAcpCompleteSts ==
- /\
- flg_comm_active' = FALSE /\
- flg_got_cli_nonce' = FALSE /\
- flg_sent_serv_nonce' = FALSE /\
- flg_sent_cert' = FALSE /\
- flg_got_premaster' = FALSE /\
- flg_set_cmn_key' = FALSE /\
- flg_done_hs_verify' = FALSE /\
- flg_sent_hs_verify' = FALSE /\
- flg_cipher_on' = FALSE /\
- flg_allow_user_auth' = FALSE /\
- flg_done_user_auth' = FALSE /\
- flg_allow_user_data' = FALSE /\
-
- flg_allow_send_data' = FALSE /\
- flg_allow_recv_data' = FALSE
- /\ UNCHANGED <<flg_tx_msg_encoded,flg_tx_add_mac,flg_rx_msg_decoded,flg_rx_chk_mac,auth_fail_cnt,recent_auth_tim>>
-
-(* Set status of user data receiving *)
-SetFlgRx ==
- /\ flg_allow_user_data = TRUE /\
- flg_allow_recv_data '= TRUE /\
- flg_rx_msg_decoded' = TRUE /\
- flg_rx_chk_mac' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,auth_fail_cnt,recent_auth_tim>>
-
-
-
-ResetFlgRx ==
- /\
- flg_allow_recv_data' = FALSE /\
- flg_rx_msg_decoded' = FALSE /\
- flg_rx_chk_mac' = FALSE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,auth_fail_cnt,recent_auth_tim>>
-
-
- (* Set status of user data transmitting *)
-SetFlgTx ==
- /\ flg_allow_user_data = TRUE /\
- flg_allow_send_data' = TRUE /\
- flg_tx_msg_encoded' = TRUE /\
- flg_tx_add_mac' = TRUE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-ResetFlgTx ==
- /\
- flg_allow_send_data' = FALSE /\
- flg_tx_msg_encoded' = FALSE /\
- flg_tx_add_mac' = FALSE
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-SetAuthInf(usr, tim, cnt) ==
- /\ usr \in INT /\ usr \in REG_USR /\ tim \in INT /\ cnt \in NAT
- /\
- auth_fail_cnt'= relational_overriding(auth_fail_cnt, {<<usr,cnt>>}) /\
- recent_auth_tim' = relational_overriding(recent_auth_tim, {<<usr, tim>>})
- /\ UNCHANGED <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data>>
-
-
-(* set https_acp complete status and reset the count of unsuccessful authentication attemps *)
-SetAuthSuccessSts(usr, cnt, tim) ==
- /\ usr \in INT /\ usr \in REG_USR /\ cnt \in NAT /\ tim \in INT
- /\
- flg_comm_active' = TRUE /\
- flg_got_cli_nonce' = TRUE /\
- flg_sent_serv_nonce' = TRUE /\
- flg_sent_cert' = TRUE /\
- flg_got_premaster' = TRUE /\
- flg_set_cmn_key' = TRUE /\
- flg_done_hs_verify' = TRUE /\
- flg_sent_hs_verify' = TRUE /\
- flg_cipher_on' = TRUE /\
- flg_allow_user_auth' = TRUE /\
- flg_done_user_auth' = TRUE /\
- flg_allow_user_data' = TRUE /\
-
- auth_fail_cnt'= relational_overriding(auth_fail_cnt, {<<usr,cnt>>}) /\
- recent_auth_tim' = relational_overriding(recent_auth_tim, {<<usr, tim>>})
- /\ UNCHANGED <<flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data>>
-
- (* Reset https_acp status and count up unsuccessful authentication attemps *)
-SetAuthFailSts(usr, cnt, tim) ==
- /\ usr \in INT /\ usr \in REG_USR /\ cnt \in NAT /\ tim \in INT
- /\
- flg_comm_active' = FALSE /\
- flg_got_cli_nonce' = FALSE /\
- flg_sent_serv_nonce' = FALSE /\
- flg_sent_cert' = FALSE /\
- flg_got_premaster' = FALSE /\
- flg_set_cmn_key' = FALSE /\
- flg_done_hs_verify' = FALSE /\
- flg_sent_hs_verify' = FALSE /\
- flg_cipher_on' = FALSE /\
- flg_allow_user_auth' = FALSE /\
- flg_done_user_auth' = FALSE /\
- flg_allow_user_data' = FALSE /\
-
- flg_allow_send_data' = FALSE /\
- flg_allow_recv_data' = FALSE /\
-
- auth_fail_cnt'= relational_overriding(auth_fail_cnt, {<<usr,cnt>>}) /\
- recent_auth_tim' = relational_overriding(recent_auth_tim, {<<usr, tim>>})
- /\ UNCHANGED <<flg_tx_msg_encoded,flg_tx_add_mac,flg_rx_msg_decoded,flg_rx_chk_mac>>
-
-
-
-allVars == <<flg_comm_active, flg_got_cli_nonce, flg_sent_serv_nonce, flg_sent_cert,flg_got_premaster,flg_set_cmn_key,flg_done_hs_verify,flg_sent_hs_verify,flg_cipher_on, flg_allow_user_auth,flg_done_user_auth,flg_allow_user_data, flg_tx_msg_encoded,flg_tx_add_mac,flg_allow_send_data,flg_rx_msg_decoded,flg_rx_chk_mac,flg_allow_recv_data,auth_fail_cnt,recent_auth_tim>>
-
-
-
-SecCtx_Next ==
- \/ SetFlgCommActive
- \/ SetFlgGotCliNonce
- \/ SetFlgSentServNonce
- \/ SetFlgSentCert
- \/ SetFlgGotPremaster
- \/ SetFlgCmnKey
- \/ SetFlgCipherOn
- \/ SetFlgDoneHsVerify
- \/ SetFlgSentHsVerify
- \/ SetFlgAllowUserAuth
- \/ SetFlgDoneUserAuth
- \/ \E usr \in REG_USR, tim \in INT: SetSuccessUserAuth(usr, tim)
- \/ \E usr \in REG_USR, tim \in INT: SetFailUserAuth(usr, tim)
- \/ SetFlgAllowUserData
- \/ SetFlgTxMsgEncoded
- \/ SetFlgTxAddMac
- \/ SetFlgAllowSendData
- \/ SetFlgRxMsgDecoded
- \/ SetFlgRxChkMac
- \/ SetFlgAllowRecvData
- \/ SetFlgsHndshkCompleteSts
- \/ ResetFlgsHndshkCompleteSts
- \/ SetFlgsAuthCompleteSts
- \/ SetFlgsAcpCompleteSts
- \/ ResetFlgsAcpCompleteSts
- \/ SetFlgRx
- \/ ResetFlgRx
- \/ SetFlgTx
- \/ ResetFlgTx
- \/ \E usr \in REG_USR, tim \in INT, cnt \in NAT: SetAuthInf(usr, tim, cnt)
- \/ \E usr \in REG_USR, tim \in INT, cnt \in NAT: SetAuthSuccessSts(usr, cnt, tim)
- \/ \E usr \in REG_USR, tim \in INT, cnt \in NAT: SetAuthFailSts(usr, cnt, tim)
-
-=============================================================================
diff --git a/src/test/resources/examples/uf50_02.tla b/src/test/resources/examples/uf50_02/uf50_02.tla
similarity index 100%
rename from src/test/resources/examples/uf50_02.tla
rename to src/test/resources/examples/uf50_02/uf50_02.tla