prism-accumulation/prism/src/explicit/AccumulationProductRegular.java

package explicit;

import java.util.ArrayList;
import java.util.BitSet;
import java.util.Vector;

import automata.finite.DeterministicFiniteAutomaton;
import automata.finite.EdgeLabel;
import automata.finite.NondeterministicFiniteAutomaton;
import automata.finite.State;
import explicit.rewards.MCRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
import parser.ast.ExpressionAccumulation;
import parser.ast.ExpressionRegular;
import prism.PrismException;
import prism.PrismSettings;

/**
 * An AccumulationProduct has ProductStates, where the first component is the
 * stateId in the original model, and the second component is the index of an
 * AccumulationTracker.
 * 
 * @author Sascha Wunderlich
 *
 * @param <M>
 */

public class AccumulationProductRegular<M extends Model> extends AccumulationProduct<M,State>
{
	DeterministicFiniteAutomaton<String> automaton;
	
	public AccumulationProductRegular(M originalModel) {
		super(originalModel);
	}
	
	public static AccumulationProductRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
		final AccumulationProductRegular<DTMC> result = new AccumulationProductRegular<DTMC>(graph);
		// Create auxiliary data
		result.createAuxData(graph, accexp, rewards, mc);
		
		// Build an operator
		class AccumulationDTMCProductOperator implements DTMCProductOperator
		{
			@Override
			public ProductState getInitialState(Integer dtmc_state)
					throws PrismException {
				int initialAccStateId = result.createInitialStateId(rewards.size());
				return new ProductState(dtmc_state, initialAccStateId);
			}

			@Override
			public ProductState getSuccessor(ProductState from_state,
					Integer dtmc_to_state) throws PrismException {
				// Get the current accumulation state
				AccumulationState<State> from_accstate = result.accStates.getById(from_state.getSecondState());
				
				// Get step weights
				double[] weights = new double[rewards.size()];
				
				for (int i=0; i < rewards.size(); i++) {
					weights[i] = rewards.get(i).getStateReward(from_state.getFirstState());
				}
				
				// Update accumulation product state, store it and get its ID.
				AccumulationState<State> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
				int to_accproduct_id = result.accStates.findOrAdd(to_accproduct);
				
				return new ProductState(dtmc_to_state, to_accproduct_id);
			}

			@Override
			public void notify(ProductState state, Integer index)
					throws PrismException {
				AccumulationState<State> accState = result.accStates.getById(state.getSecondState());
				if (result.isGoodAccState(accState, accexp, mc)) {
					result.goodStates.set(index);
				}
			}

			@Override
			public void finish() throws PrismException {
				// Do nothing
			}

			@Override
			public DTMC getGraph() {
				return graph;
			}
		}
		
		// Apply the operator
		AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator();
		ProductWithProductStates.generate(op, result, statesOfInterest);
		
		return result;
	}
	
	public static AccumulationProductRegular<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
		// This is basically the same thing as for DTMCs
		final AccumulationProductRegular<MDP> result = new AccumulationProductRegular<MDP>(graph);
		
		// Create auxiliary data
		mc.getLog().println("  [AP] generating aux data...");
		result.createAuxData(graph, accexp, rewards, mc);
		mc.getLog().println("       done.");

		class AccumulationMDPProductOperator implements MDPProductOperator
		{

			@Override
			public ProductState getInitialState(Integer MDP_state)
					throws PrismException {
				int initialAccStateId = result.createInitialStateId(rewards.size());
				return new ProductState(MDP_state, initialAccStateId);
			}

			@Override
			public ProductState getSuccessor(ProductState from_state,
					int choice_i, Integer mdp_to_state) throws PrismException {
				// Get the current accumulation state
				AccumulationState<State> from_accstate = result.accStates.getById(from_state.getSecondState());
				
				// Get step weights
				// THIS IS DIFFERENT FROM ABOVE!
				double[] weights = new double[rewards.size()];
				
				for (int i=0; i < rewards.size(); i++) {
					double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState());
					
					currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i);
					weights[i] = currentWeight;
				}

				// Update accumulation product state, store it and get its ID.
				AccumulationState<State> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
				int to_accproduct_id = result.accStates.findOrAdd(to_accproduct);
				
				return new ProductState(mdp_to_state, to_accproduct_id);
			}

			@Override
			public void notify(ProductState state, Integer index)
					throws PrismException {
				AccumulationState<State> accState = result.accStates.getById(state.getSecondState());
				if (result.isGoodAccState(accState, accexp, mc)) {
					result.goodStates.set(index);
				}
			}

			@Override
			public void finish() throws PrismException {
				// Do nothing
				
			}

			@Override
			public MDP getGraph() {
				return graph;
			}
		}
		
		AccumulationMDPProductOperator op = new AccumulationMDPProductOperator();
		ProductWithProductStates.generate(op, result, statesOfInterest);
		return result;
	}
	
	@Override
	protected boolean isFinalTrack(AccumulationTrack<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
		boolean isFinal = false;
		if ( track != null ) {
				isFinal = automaton.isAcceptingState(track.getComponent());
		}
		
		return isFinal;
	}
	
	@Override
	protected State getInitialComponent() {
		return automaton.getInitialState();
	}
	
	@Override
	protected AccumulationTrack<State> updateTrack(Integer modelFromStateId, AccumulationTrack<State> track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) {
		State currentState = track.getComponent();
		
		// Build EdgeLabel from labels.
		// labels is a BitSet with labels L0,...,Ln
		
		ArrayList<String> edgeSymbols = new ArrayList<>();
		BitSet edgeValues = new BitSet();
		
		for (int i=0; i < labels.size(); i++) {
			// Each bitLabel contains one L
			edgeSymbols.add(i, "L"+i);
			if(labels.get(i).get(modelFromStateId)) {
				edgeValues.set(i);
			}
		}

		EdgeLabel<String> edgeLabel = new EdgeLabel<>(edgeSymbols, edgeValues);
		
		State nextState = automaton.getSuccessor(currentState,edgeLabel);
		//System.out.println("Successor of " + currentState + " via " + edgeLabel + ":" + nextState);
		
		// Undefined behavior, return the null-Track
		if (nextState == null) { return null; }
		
		// If we have defined behavior, update the weights and get the new stateId.
		double[] newweights = new double[weights.length];
		for (int i = 0; i < weights.length; i++) {
			newweights[i] = weights[i] + track.getWeights()[i];
		}
		
		return new AccumulationTrack<State>(newweights, nextState);
	}
	
	/**
	 * Populates fields:
	 * - automaton with a trimmed deterministic finite automaton,
	 * - numberOfTracks  with the length of its longest path plus one, and
	 * - numberOfWeights with the size of the reward vector.
	 * 
	 * @param graph
	 * @param accexp
	 * @param mc
	 * @throws PrismException
	 */
	protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException {
		// Build labels and DFA
		AccumulationModelChecker accMc = new AccumulationModelChecker();
		ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels);
		
		// Create and store the actual DFA
		NondeterministicFiniteAutomaton<String> nfa = NondeterministicFiniteAutomaton.fromExpressionRegular(reg);
		//System.out.println(nfa.toDot());
		
		automaton = nfa.determinize();
		automaton.trim(); // This should remove cycles.
		
		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
		  nfa.exportToDotFile("DEBUG-automaton-nfa.dot");
		}
		
		if (!automaton.isAcyclic()) {
			throw new PrismException("Cannot handle cyclic automata!");
		}
		
		numberOfTracks = automaton.getLongestPathLength()+1;
		numberOfWeights= rewards.size();
	}
}