Skip to content
Snippets Groups Projects
Select Git revision
  • 9658b39544947d6a0c6155a920d4adaa11f5970f
  • 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

RecursiveFunktion.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    ExpressionConstantTest.java 1.59 KiB
    package de.b2tla.analysis;
    
    import static de.b2tla.util.TestUtil.compare;
    
    import org.junit.Test;
    
    public class ExpressionConstantTest {
    
    	@Test
    	public void testAConstantIsconstant() throws Exception {
    		String machine = "MACHINE test\n"
    				+ "CONSTANTS k \n"
    				+ "PROPERTIES k = 1 & !x.(x = k => 1 = 1)\n" + "END";
    		
    		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
    				+ "k == 1 \n"
    				+ "ASSUME \\A x \\in {k} : x = k => 1 = 1 \n"
    				+ "======";
    		compare(expected, machine);
    	}
    	
    	@Test
    	public void testAConstantIsconstant2() throws Exception {
    		String machine = "MACHINE test\n"
    				+ "CONSTANTS k, k2 \n"
    				+ "PROPERTIES k = k2 & k2 = 1 \n" + "END";
    		
    		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
    				+ "k2 == 1 \n"
    				+ "k == k2 \n"
    				+ "======";
    		compare(expected, machine);
    	}
    	
    	@Test
    	public void testBoundedVariable() throws Exception {
    		String machine = "MACHINE test\n"
    				+ "PROPERTIES !x.(x = 1 => !y.(y= x => 1 = 1))\n" + "END";
    		
    		String expected = "---- MODULE test----\n" + "EXTENDS Integers\n"
    				+ "ASSUME \\A x \\in {1} : x = 1 => \\A y \\in {x} : y = x => 1 = 1 \n"
    				+ "======";
    		compare(expected, machine);
    	}
    	
    	@Test
    	public void testNotConstantBoundedVariable() throws Exception {
    		String machine = "MACHINE test\n"
    				+ "PROPERTIES !x,y.(x = y & y = 1 => 1 = 1)\n" + "END";
    		
    		String expected = "---- MODULE test----\n"
    				+ "EXTENDS Integers \n"
    				+ "ASSUME \\A x \\in (-1..4), y \\in {1} : x = y => 1 = 1 \n"
    				+ "======";
    		compare(expected, machine);
    	}
    	
    }