Skip to content
Snippets Groups Projects
Select Git revision
  • e13611ad5a332e6e73ec25fb60523a75ab59eaee
  • master default protected
  • release/1.1.4
  • release/1.1.3
  • release/1.1.1
  • 1.4.2
  • 1.4.1
  • 1.4.0
  • 1.3.0
  • 1.2.1
  • 1.2.0
  • 1.1.5
  • 1.1.4
  • 1.1.3
  • 1.1.1
  • 1.1.0
  • 1.0.9
  • 1.0.8
  • 1.0.7
  • v1.0.5
  • 1.0.5
21 results

SimpleExpressionTest.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");
    	}
    }