Your First Plugin

Create Your First Plugin for EPMC

The easiest way to create your first plugin under the directory plugins is to copy one plugin, say propertysolver-pctl and make following changes. Suppose the name of your plugin is propertysolver-reachability, you should do the following:

• In pom.xml, you should replace propertysolver-pctl with propertysolver-reachability;
• In MANIFEST.mf under resource folder, you should change the plugin name and plugin dependencies accordingly;
• In .project, you should change project name accordingly.

Once you have done above changes, you are ready to implement your own plugin. Suppose you are going to implement a model checker which only handles formula P=? [F p] over DTMCs. Note that every probabilistic model checker is required to implement the PropertySolver interface.

public final class PropertySolverExplicitReachability implements PropertySolver {
    /**
    	give the identifier for your property solver, in ePMC
    	we recommend you to first give the solver name and then engine name
    */

    public final static String IDENTIFIER = "reachability-explicit";

	/**
    	give the identifier for your property solver, in ePMC
    	we recommend you to first give the solver name and then engine name
    */
    @Override
    public String getIdentifier() {
        return IDENTIFIER;
    }

	/** setModelchecker will be called by the main program
	    to establish the procedure for model checking */
    @Override
    public void setModelChecker(ModelChecker modelChecker) {
        assert modelChecker != null;
        this.modelChecker = modelChecker;
        if (modelChecker.getEngine() instanceof EngineExplicit) {
        	this.graph = modelChecker.getLowLevel();
        }
        // no need to use contextExpression
        //this.contextExpression = modelChecker.getContextExpression();
        this.contextValue = modelChecker.getModel().getContextValue();
    }

	@Override
	public void setProperty(Expression property) {
		this.property = property;
	}

	// initial states
	@Override
	public void setForStates(StateSet forStates) {
		this.forStates = forStates;
	}

	/**
	 * main program will call this function to solve the model checking problem
	 * */
    @Override
    public StateMap solve() throws EPMCException {
        assert property != null;
        assert forStates != null;
        assert property instanceof ExpressionQuantifier;
        StateSetExplicit forStatesExplicit = (StateSetExplicit) forStates;
        graph.explore(forStatesExplicit.getStatesExplicit());
        ExpressionQuantifier propertyQuantifier = (ExpressionQuantifier) property;
        // remove P=? part, get F a
        Expression quantifiedProp = propertyQuantifier.getQuantified();
        // doSolve does the model checking
        StateMap result = doSolve(quantifiedProp, forStates);
        //StateMap stores the reachability probabilities for every state in the graph
        return result;
    }

    /** collect the states which satisfy a */
    private StateMap doSolve(Expression property, StateSet states)
            throws EPMCException {
        // set states we are interested in
    	this.computeForStates = (StateSetExplicit) states;

    	// use propertysolver propositional to check the innners
        StateSet allStates = UtilGraph.computeAllStatesExplicit(modelChecker.getLowLevel());
        Set<Expression> inners = UtilReachability.collectReachabilityInner(property);
        for (Expression inner : inners) {
            StateMapExplicit innerResult = (StateMapExplicit) modelChecker.check(inner, allStates);
            UtilGraph.registerResult(graph, inner, innerResult);
        }
        allStates.close();

        BitSet oneStates = UtilBitSet.newBitSetUnbounded();        
        // collect all states which satisfied the propositional formula property
        Expression[] expressions = inners.toArray(new Expression[0]);
        Value[] evalValues = new Value[expressions.length];
        for (int varNr = 0; varNr < expressions.length; varNr++) {
            evalValues[varNr] = expressions[varNr].getType(modelChecker.getLowLevel()).newValue();
        }

        ExpressionTemporal propertyTemporal = (ExpressionTemporal)property;
        // evaluator for propositional formula a out of F a
        EvaluatorExplicitBoolean evaluator = UtilEvaluatorExplicit.newEvaluatorBoolean(
        		propertyTemporal.getOperand1(), graph, expressions);

        for (int node = 0; node < graph.getNumNodes(); node ++) {
            graph.queryNode(node);
            // collect the truth value of all atomic propositions in this state
            for (int exprNr = 0; exprNr < expressions.length; exprNr++) {
                evalValues[exprNr] = graph.getNodeProperty(expressions[exprNr]).get();
            }

            // check whether current state satisfies a out of F a
            // under the satisfaction values of inners
            boolean sat = evaluator.evaluateBoolean(evalValues);

            if (sat)  oneStates.set(node);

        }
        Log log = graph.getOptions().get(OptionsMessages.LOG);
        log.send(MessagesReachability.REACHABILITY_NUM_ONE_STATES, graph.getNumNodes(), oneStates.cardinality());
        // compute the reachability probabilities for every state in the model
        ValueArrayAlgebra results = UtilReachability.computeReachabilityProbability(graph, oneStates);
        return prepareStateMap(results);
    }



    /** get results for states we are interested in */
    private StateMap prepareStateMap(ValueArrayAlgebra values) {
    	TypeArray typeArray = TypeWeight.get(contextValue).getTypeArray();
    	ValueArray resultValues = UtilValue.newArray(typeArray, computeForStates.size());
    	TypeAlgebra typeWeight = TypeWeight.get(contextValue);
        Value val = typeWeight.newValue();
        for (int i = 0; i < computeForStates.size(); i++) {
            values.get(val, i);
            resultValues.set(val, i);
        }

        return UtilGraph.newStateMap(computeForStates.clone(), resultValues);
    }

    /**
     * this function determine whether the propertysolver can handle the model checking task
     * */
    @Override
    public boolean canHandle() throws EPMCException {
        assert property != null;
        if (!(modelChecker.getEngine() instanceof EngineExplicit)) {
            return false;
        }

        Semantics semantics = modelChecker.getModel().getSemantics();
        // only allow DTMC
        if (! SemanticsDTMC.isDTMC(semantics)) {
        	return false;
        }
        // has P=? quantifier
        if (!(property instanceof ExpressionQuantifier)) {
            return false;
        }

        ExpressionQuantifier propertyQuantifier = (ExpressionQuantifier) property;
        // only allow F a
        if (!UtilReachability.isReachability(propertyQuantifier.getQuantified())) {
            return false;
        }

        // check whether atomic propositions can be handled by propertysolver-propositional (if exists)
        Set<Expression> inners = UtilReachability.collectReachabilityInner(propertyQuantifier.getQuantified());
        StateSet allStates = UtilGraph.computeAllStatesExplicit(modelChecker.getLowLevel());
        for (Expression inner : inners) {
            modelChecker.ensureCanHandle(inner, allStates);
        }
        if (allStates != null) {
        	allStates.close();
        }
        return true;
    }


    // ---------------- some functions which are used for building the model graph
	@Override
    public Set<Object> getRequiredGraphProperties() throws EPMCException {
    	Set<Object> required = new LinkedHashSet<>();
    	// semantics for the graph (MDP, MC and etc.)
    	required.add(CommonProperties.SEMANTICS);
    	return required;
    }

    @Override
    public Set<Object> getRequiredNodeProperties() throws EPMCException {
    	// for node properties
    	Set<Object> required = new LinkedHashSet<>();
    	// STATE and PLAYER properties are required for all models
    	// will be used in compute SCCs
    	required.add(CommonProperties.STATE);
    	required.add(CommonProperties.PLAYER);

    	ExpressionQuantifier propertyQuantifier = (ExpressionQuantifier) property;
    	// collect atomic propositions in the formula
        Set<Expression> inners = UtilReachability.collectReachabilityInner(propertyQuantifier.getQuantified());
        // get the state set in graph
        StateSet allStates = UtilGraph.computeAllStatesExplicit(modelChecker.getLowLevel());
        // evaluate the satisfaction for all atomic propositions in the states
        for (Expression inner : inners) {
        	required.addAll(modelChecker.getRequiredNodeProperties(inner, allStates));
        }
    	return required;
    }

    @Override
    public Set<Object> getRequiredEdgeProperties() throws EPMCException {
    	Set<Object> required = new LinkedHashSet<>();
    	// require the edges of constructed graph being labelled by weights (probabilities)
    	required.add(CommonProperties.WEIGHT);
    	return required;
    }
}