Skip to content
Snippets Groups Projects
Commit 1519ab96 authored by hansen's avatar hansen
Browse files

Fixed a Bug finding an Assertion Error

parent bdcd30d1
Branches
Tags
No related merge requests found
Showing
with 297 additions and 65 deletions
......@@ -42,7 +42,7 @@ test {
task integrationtests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
include('de/b2tla/tlc/integration/**')
include('de/b2tla/tlc/integration/probprivate/**')
}
jar { from sourceSets.main.allJava }
......
......@@ -82,7 +82,6 @@ public class TLCRunner {
} catch (InterruptedException e) {
e.printStackTrace();
}
return stdOut.getLog();
}
......
......@@ -23,6 +23,7 @@ import de.b2tla.btypes.FunctionType;
import de.b2tla.btypes.IntegerType;
import de.b2tla.btypes.PairType;
import de.b2tla.btypes.SetType;
import de.b2tla.btypes.UntypedType;
import de.b2tla.ltl.LTLFormulaVisitor;
import de.b2tla.tla.ConfigFile;
import de.b2tla.tla.TLADefinition;
......@@ -1590,6 +1591,9 @@ public class TLAPrinter extends DepthFirstAdapter {
@Override
public void caseATotalFunctionExpression(ATotalFunctionExpression node) {
BType type = this.typechecker.getType(node);
if(type == null){
type = new SetType(new FunctionType(new UntypedType(), new UntypedType()));
}
BType subtype = ((SetType) type).getSubtype();
if (subtype instanceof FunctionType) {
tlaModuleString.append("[");
......
......@@ -260,13 +260,14 @@ public class Generator extends DepthFirstAdapter {
init = true;
this.tlaModule.variables.add(con);
BType type = typechecker.getType(con);
PExpression n = type.createSyntaxTreeNode();
AMemberPredicate member = new AMemberPredicate(
(PExpression) con.clone(),
type.createSyntaxTreeNode());
(PExpression) con.clone(), n);
ArrayList<NodeType> list = this.typeRestrictor.getRestrictedTypesSet(con);
ArrayList<NodeType> list = this.typeRestrictor
.getRestrictedTypesSet(con);
if (list == null || list.size() == 0) {
System.out.println(con);
tlaModule.addInit(member);
} else {
......
......@@ -22,8 +22,7 @@ public class TLCOutput {
String parseError;
public static enum TLCResult {
Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError,
PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
Deadlock, Goal, InvariantViolation, ParseError, NoError, AssertionError, PropertiesError, EnumerateError, TLCError, TemporalProperty, WellDefinednessError
}
public long getRunningTime() {
......@@ -143,7 +142,10 @@ public class TLCOutput {
public static TLCResult findError(ArrayList<String> list) {
for (int i = 0; i < list.size(); i++) {
String m = list.get(i);
if (m.startsWith("Error:") || m.startsWith("\"Error:")) {
if (m.startsWith("Error:") || m.startsWith("\"Error:")
|| m.startsWith("The exception was a")) {
TLCResult res = findError(m);
if (res != null)
return findError(m);
}
}
......@@ -163,19 +165,23 @@ public class TLCOutput {
} else if (invName.startsWith("Assertion")) {
return TLCResult.AssertionError;
}
} else if (m.contains("The invariant of Assertion")) {
return TLCResult.AssertionError;
} else if (res[1].equals("Assumption")) {
return TLCResult.PropertiesError;
} else if (res[1].equals("Temporal")) {
return TLCResult.TemporalProperty;
} else if (m.equals("Error: TLC threw an unexpected exception.")) {
return TLCResult.TLCError;
return null;
} else if (m.startsWith("\"Error: Invalid function call to relation")) {
return TLCResult.WellDefinednessError;
} else if (m.startsWith("Error: The behavior up to")) {
return null;
} else if (m.startsWith("Error: The following behavior constitutes a counter-example:")) {
} else if (m
.startsWith("Error: The following behavior constitutes a counter-example:")) {
return null;
}else if (m.startsWith("Error: The error occurred when TLC was evaluating the nested")) {
} else if (m
.startsWith("Error: The error occurred when TLC was evaluating the nested")) {
return null;
}
return TLCResult.TLCError;
......
package de.b2tla.tlc.integration;
import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static org.junit.Assert.assertEquals;
import org.junit.BeforeClass;
......@@ -7,7 +8,6 @@ import org.junit.Test;
import de.b2tla.B2TLA;
import de.b2tla.B2TLAGlobals;
import de.b2tla.tlc.TLCOutput;
public class ErrorTest {
......@@ -19,19 +19,19 @@ public class ErrorTest {
@Test
public void testInvariantError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" };
assertEquals(TLCOutput.TLCResult.InvariantViolation, B2TLA.test(a,true));
assertEquals(InvariantViolation, B2TLA.test(a,true));
}
@Test
public void testDeadlock() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/Deadlock.mch" };
assertEquals(TLCOutput.TLCResult.Deadlock, B2TLA.test(a,true));
assertEquals(Deadlock, B2TLA.test(a,true));
}
@Test
public void testPropertiesError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/PropertiesError.mch" };
assertEquals(TLCOutput.TLCResult.PropertiesError, B2TLA.test(a,true));
assertEquals(PropertiesError, B2TLA.test(a,true));
}
@Test
......@@ -43,13 +43,26 @@ public class ErrorTest {
@Test
public void testNoError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/NoError.mch" };
assertEquals(TLCOutput.TLCResult.NoError, B2TLA.test(a,true));
assertEquals(NoError, B2TLA.test(a,true));
}
@Test
public void testEnumerationError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/EnumerationError.mch" };
assertEquals(TLCOutput.TLCResult.TLCError, B2TLA.test(a,true));
assertEquals(TLCError, B2TLA.test(a,true));
}
@Test
public void testAssertionError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/AssertionError.mch" };
assertEquals(AssertionError, B2TLA.test(a,true));
}
@Test
public void testConstantAssertionError() throws Exception {
String[] a = new String[] { "./src/test/resources/errors/AssertionError2.mch" };
assertEquals(AssertionError, B2TLA.test(a,true));
}
}
package de.b2tla.tlc.integration;
import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
import static org.junit.Assert.assertEquals;
import org.junit.Test;
import de.b2tla.B2TLA;
import de.b2tla.B2TLAGlobals;
public class SingleConfigurations {
// @Test
// public void TautologiesPl() throws Exception {
// B2TLAGlobals.setDeleteOnExit(true);
// String[] a = new String[] { "../probprivate/public_examples/TLC/others/TautologiesPL.mch", "-nodead"};
// assertEquals(NoError, B2TLA.test(a));
// }
}
\ No newline at end of file
package de.b2tla.tlc.integration;
package de.b2tla.tlc.integration.probprivate;
import static org.junit.Assert.*;
import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static de.b2tla.tlc.TLCOutput.TLCResult.AssertionError;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
......@@ -9,21 +9,21 @@ import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.*;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
import de.b2tla.B2TLA;
import de.b2tla.B2TLAGlobals;
@RunWith(PolySuite.class)
public class ProBPrivateTests extends AbstractParseMachineTest {
public class AssertionErrorTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public ProBPrivateTests(File machine, TLCResult result) {
public AssertionErrorTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
......@@ -31,20 +31,13 @@ public class ProBPrivateTests extends AbstractParseMachineTest {
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
assertEquals(error, B2TLA.test(a,true));
assertEquals(error, B2TLA.test(a, false));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(InvariantViolation, "../probprivate/public_examples/TLC/InvariantViolation"));
list.add(new TestPair(Deadlock, "../probprivate/public_examples/TLC/Deadlock"));
list.add(new TestPair(Goal, "../probprivate/public_examples/TLC/GOAL"));
list.add(new TestPair(NoError, "../probprivate/public_examples/TLC/NoError"));
list.add(new TestPair(AssertionError, "../probprivate/public_examples/TLC/AssertionError"));
return getConfiguration(list);
}
}
package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.Deadlock;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class DeadlockTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public DeadlockTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
assertEquals(error, B2TLA.test(a, true));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(Deadlock,
"../probprivate/public_examples/TLC/Deadlock"));
return getConfiguration(list);
}
}
package de.b2tla.tlc.integration.probprivate;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class GoalTest extends AbstractParseMachineTest{
private final File machine;
private final TLCResult error;
public GoalTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath()};
assertEquals(error, B2TLA.test(a,false));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(TLCResult.Goal, "../probprivate/public_examples/TLC/GOAL"));
return getConfiguration(list);
}
}
package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.InvariantViolation;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class InvariantViolationTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public InvariantViolationTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
assertEquals(error, B2TLA.test(a, true));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(InvariantViolation,
"../probprivate/public_examples/TLC/InvariantViolation"));
return getConfiguration(list);
}
}
package de.b2tla.tlc.integration;
package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.*;
import static org.junit.Assert.assertEquals;
......
package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.NoError;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class NoErrorTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public NoErrorTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
assertEquals(error, B2TLA.test(a, true));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(NoError,
"../probprivate/public_examples/TLC/NoError"));
return getConfiguration(list);
}
}
package de.b2tla.tlc.integration.probprivate;
import static de.b2tla.tlc.TLCOutput.TLCResult.WellDefinednessError;
import static org.junit.Assert.assertEquals;
import java.io.File;
import java.util.ArrayList;
import org.junit.Test;
import org.junit.runner.RunWith;
import de.b2tla.B2TLA;
import de.b2tla.tlc.TLCOutput.TLCResult;
import de.b2tla.util.AbstractParseMachineTest;
import de.b2tla.util.PolySuite;
import de.b2tla.util.TestPair;
import de.b2tla.util.PolySuite.Config;
import de.b2tla.util.PolySuite.Configuration;
@RunWith(PolySuite.class)
public class WellDefinednessTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public WellDefinednessTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
@Test
public void testRunTLC() throws Exception {
String[] a = new String[] { machine.getPath() };
assertEquals(error, B2TLA.test(a,true));
}
@Config
public static Configuration getConfig() {
final ArrayList<TestPair> list = new ArrayList<TestPair>();
list.add(new TestPair(WellDefinednessError, "../probprivate/public_examples/TLC/WellDefinednessError"));
return getConfiguration(list);
}
}
MACHINE AssertionError
ASSERTIONS x = 1
VARIABLES x
INVARIANT x : 1..2
INITIALISATION x := 1
OPERATIONS
foo = PRE x = 1 THEN x:= 2 END
END
\ No newline at end of file
MACHINE AssertionError
ASSERTIONS 2 = 1
VARIABLES x
INVARIANT x : 1..2
INITIALISATION x := 1
OPERATIONS
foo = PRE x = 1 THEN x:= 2 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