Skip to content
Snippets Groups Projects
Select Git revision
  • 65c6345a4528491c4e4b3924efe15a6d6d24f311
  • master default protected
  • exec_auto_adjust_trace
  • let_variables
  • v1.4.1
  • v1.4.0
  • v1.3.0
  • v1.2.0
  • v1.1.0
  • v1.0.0
10 results

ProBKernel.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    SimpleExpressionTest.java 1.02 KiB
    /**
     * @author Dominik Hansen <Dominik.Hansen at hhu.de>
     **/
    
    package de.tla2b.expression;
    
    import org.junit.Test;
    
    import static de.tla2b.util.TestUtil.compareExpr;
    
    public class SimpleExpressionTest {
    
    	@Test
    	public void testSimpleExpression() throws Exception {
    		compareExpr("1 + 2", "1 + 2");
    	}
    
    	@Test
    	public void testSimplePredicate() throws Exception {
    		compareExpr("1 = 1", "1 = 1");
    	}
    
    	@Test
    	public void testSimplePredicate2() throws Exception {
    		compareExpr("1 < 1", "1 < 1");
    	}
    
    	@Test
    	public void testModulIntegers() throws Exception {
    		compareExpr("-1 : INTEGER", "-1 \\in Int");
    	}
    
    	@Test
    	public void testExist() throws Exception {
    		compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1");
    	}
    
    	@Test
    	public void testIfThenElse() throws Exception {
    		compareExpr(
    				"(%t_.( t_ = 0 & 1 = 1 | 1 )\\/%t_.( t_ = 0 & not(1 = 1) | 2 ))(0)",
    				"IF 1 = 1 THEN 1 ELSE 2");
    	}
    
    	@Test
    	public void testTRUE() throws Exception {
    		compareExpr("TRUE", "TRUE");
    	}
    }