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

RecursiveDefinition.java

  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    RecursiveDefinition.java 961 B
    package de.tla2b.analysis;
    
    import de.tla2b.exceptions.NotImplementedException;
    import tla2sany.semantic.OpApplNode;
    import tla2sany.semantic.OpDefNode;
    import tlc2.tool.BuiltInOPs;
    
    public class RecursiveDefinition extends BuiltInOPs {
    
    	private final OpDefNode def;
    	private OpApplNode ifThenElse;
    
    	public RecursiveDefinition(OpDefNode def) throws NotImplementedException {
    		this.def = def;
    		evalRecursiveDefinition();
    	}
    
    	private void evalRecursiveDefinition() throws NotImplementedException {
    		if (def.getBody() instanceof OpApplNode) {
    			OpApplNode o = (OpApplNode) def.getBody();
    			if (getOpCode(o.getOperator().getName()) == OPCODE_ite) {// IF THEN ELSE
    				ifThenElse = o;
    				return;
    			}
    		}
    		throw new NotImplementedException(
    			"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
    	}
    
    	public OpDefNode getOpDefNode() {
    		return def;
    	}
    
    	public OpApplNode getIfThenElse() {
    		return ifThenElse;
    	}
    }