Skip to content
Snippets Groups Projects
Commit 346b1111 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

add two tests

negation ~ and missing Init
parent d43d54a0
Branches
Tags
No related merge requests found
Pipeline #148576 passed
package de.tla2b.prettyprintb;
import de.tla2b.exceptions.SemanticErrorException;
import org.junit.Ignore;
import org.junit.Test;
......@@ -63,4 +64,15 @@ public class ActionsTest {
+ "END";
compare(expected, module);
}
@Test(expected = SemanticErrorException.class)
public void testMissingInit() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Next == x'=x+1 \n"
+ "=================================";
compare("MACHINE Testing END", module);
}
}
......@@ -80,6 +80,19 @@ public class LogicOperatorsTest {
compare(expected, module);
}
@Test
public void testNegation2() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "CONSTANTS a,b \n"
+ "ASSUME a \\in BOOLEAN /\\ b = ~a \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "CONSTANTS a, b \n"
+ "PROPERTIES a : BOOL & b : BOOL & (a : BOOL & b = bool(not(a = TRUE))) \n" + "END";
compare(expected, module);
}
/*
* Implication and Equivalence: =>, \equiv
*/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment