gt:         actionCube = buildActionCube(actionVariable);
context: /****************************************************************************
  
      ePMC - an extensible probabilistic model checker
      Copyright (C) 2017
  
      This program is free software: you can redistribute it and/or modify
      it under the terms of the GNU General Public License as published by
      the Free Software Foundation, either version 3 of the License, or
      (at your option) any later version.
  
      This program is distributed in the hope that it will be useful,
      but WITHOUT ANY WARRANTY; without even the implied warranty of
      MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
      GNU General Public License for more details.
  
      You should have received a copy of the GNU General Public License
      along with this program.  If not, see <http://www.gnu.org/licenses/>.
  
   *****************************************************************************/
  
  package epmc.jani.dd;
  
  import static epmc.error.UtilError.ensure;
  
  import java.util.ArrayList;
  import java.util.Collections;
  import java.util.LinkedHashMap;
  import java.util.LinkedHashSet;
  import java.util.List;
  import java.util.Map;
  import java.util.Set;
  
  import epmc.dd.ContextDD;
  import epmc.dd.DD;
  import epmc.dd.Permutation;
  import epmc.dd.VariableDD;
  import epmc.expression.Expression;
  import epmc.expression.standard.UtilExpressionStandard;
  import epmc.expression.standard.evaluatordd.ExpressionToDD;
  import epmc.graph.CommonProperties;
  import epmc.graph.LowLevel;
  import epmc.graph.Player;
  import epmc.graph.Semantics;
  import epmc.graph.SemanticsDiscreteTime;
  import epmc.graph.SemanticsNonDet;
  import epmc.graph.dd.GraphDD;
  import epmc.graph.dd.GraphDDProperties;
  import epmc.graph.explorer.Explorer;
  import epmc.jani.model.ModelJANI;
  import epmc.jani.model.OptionsJANIModel;
  import epmc.jani.model.UtilModelParser;
  import epmc.jani.model.Variable;
  import epmc.modelchecker.Engine;
  import epmc.modelchecker.Model;
  import epmc.options.Options;
  import epmc.value.Type;
  import epmc.value.TypeEnum;
  import epmc.value.TypeInteger;
  import epmc.value.TypeObject;
  import epmc.value.Value;
  
  // TODO check memory usage, in particular in case of errors
  // TODO correct handling of graph/node/edge properties
  //AT: there are no transient/observable assignment in the JANI specification
  // TODO observables
  
  /**
   * DD-based symbolic graph representation of a JANI model.
   * 
   * @author Ernst Moritz Hahn
   */
  public final class GraphDDJANI implements GraphDD {
      public final static String IDENTIFIER = "jani-dd";
      
      public final static class Builder implements LowLevel.Builder {
          private Model model;
          private Engine engine;
          private final Set<Object> graphProperties = new LinkedHashSet<>();
          private final Set<Object> nodeProperties = new LinkedHashSet<>();
          private final Set<Object> edgeProperties = new LinkedHashSet<>();
  
          @Override
          public Builder setModel(Model model) {
              this.model = model;
              return this;
          }
  
          @Override
          public Builder setEngine(Engine engine) {
              this.engine = engine;
              return this;
          }
  
          @Override
          public Builder addGraphProperties(Set<Object> graphProperties) {
              this.graphProperties.addAll(graphProperties);
              return this;
          }
  
          @Override
          public Builder addNodeProperties(Set<Object> nodeProperties) {
              this.nodeProperties.addAll(nodeProperties);
              return this;
          }
  
          @Override
          public Builder addEdgeProperties(Set<Object> edgeProperties) {
              this.edgeProperties.addAll(edgeProperties);
              return this;
          }
  
          @Override
          public GraphDDJANI build() {
              if (!(engine instanceof Explorer)) {
                  return null;
              }
              if (!(model instanceof ModelJANI)) {
                  return null;
              }
              return new GraphDDJANI(this);
          }
      }
      
      /** Encoding marker of present state variables. */
      private final static int PRES_STATE = 0;
      /** Encoding marker of next state variables. */
      private final static int NEXT_STATE = 1;
      /** String "action". */
      private final static String ACTION = "action";
      /** String containing an underscore. */
      private static final String UNDERSCORE = "_";
  
      /** Whether graph was already closed and cannot be used further. */
      private boolean closed;
      /** JANI model which this object represents. */
      private final ModelJANI model;
      /** DD context of this graph, derived from model. */
      private final ContextDD contextDD;
      /** DD variables used to build the variable for the action chosen. */
      private List<List<DD>> ddActionBits;
      /** List of global DD variables. */
      private final List<VariableDD> globalVariableDDs = new ArrayList<>();
      /** Map from global variables to DD variables. */
      private final Map<Variable,VariableDD> globalVariableToDD = new LinkedHashMap<>();
      /** Unmodifiable map from global variables to DD variables. */
      private final Map<Variable,VariableDD> globalVariablesToDDExternal = Collections.unmodifiableMap(globalVariableToDD);
      /** Map from global variable identifiers to DD variables. */
      private final Map<Expression,VariableDD> globalIdentifierToDD = new LinkedHashMap<>();
      /** Unmodifiable map from global variable identifiers to DD variables. */
      private final Map<Expression,VariableDD> globalIdentifierToDDExternal = Collections.unmodifiableMap(globalIdentifierToDD);
      /** Map from global variables to variable identifiers. */
      private final Map<Variable,Expression> globalVariableToIdentifier = new LinkedHashMap<>();
      /** Unmodifiable map from global variables to variable identifiers. */
      private final Map<Variable,Expression> globalVariableToIdentifierExternal = Collections.unmodifiableMap(globalVariableToIdentifier);
      /** Initial nodes of the graph. */
      private final DD initialNodes;
      /** Cube of present state variables. */
      private DD presCube;
      /** Cube of next state variables. */
      private DD nextCube;
      /** Cube of action variables (encoding choice of edges). */
      private final DD actionCube;
      /** Permutation to swap present and next state variables. */
      private final Permutation swapPresNext;
      /** Final transition relation - DD, not */
      private final DD transitions;
      /** Node space of this graph. */
      private final DD nodeSpace;
      /** Properties of this graph. */
      private final GraphDDProperties properties = new GraphDDProperties(this);
      /** Converter from expressions to their symbolic representations. */
      private ExpressionToDD expressionToDD;
  
      private GraphDDJANI(Builder builder) {
          this((ModelJANI) builder.model, builder.nodeProperties, builder.edgeProperties);
      }
  
      /**
       * Construct a new symbolic graph from the given JANI model.
       * None of the parameters may be {@code null} or contain {@code null}
       * entries.
       * 
       * @param model model to construct symbolic representation of
       * @param nodeProperties node properties to be derived and stored
       * @param edgeProperties edge properties to be derived and stored
       */
      public GraphDDJANI(ModelJANI model,
              Set<Object> nodeProperties,
              Set<Object> edgeProperties) {
          assert assertConstructor(nodeProperties, edgeProperties);
  
          this.model = model;
          this.contextDD = ContextDD.get();
          prepareActionDDVariable();
          buildGlobalVariables();
          expressionToDD = new ExpressionToDD(globalIdentifierToDD);
          PreparatorDDComponent preparator = new PreparatorDDComponent();
          DDComponent component = preparator.prepare(this, model.getSystem());
  
          initialNodes = buildInitialNodes(component);
          presCube = buildPresCube(component);
          nextCube = buildNextCube(component);
  
          List<DDTransition> transitions = buildTransitions(component);
          swapPresNext = contextDD.newPermutationCube(presCube, nextCube);
          nodeSpace = explore(transitions);
          DD deadlocks = buildDeadlocks(transitions);
          DDTransition deadlockTransition = null;
          if (!deadlocks.isFalse()) {
              ensure(Options.get().getBoolean(OptionsJANIModel.JANI_FIX_DEADLOCKS), ProblemsJANIDD.JANI_DD_DEADLOCK);
              deadlockTransition = computeDeadlockTransition(deadlocks, component.getVariables());
          }
          deadlocks.dispose();
          checkStateSpace(transitions);
          if (deadlockTransition != null) {
              transitions.add(deadlockTransition);
          }
          VariableDD actionVariable = buildActionVariable(transitions);
          DD weight = buildWeight(transitions, actionVariable);
  
  