s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

explicit.LTSNBAProduct: Construct and store the product of a model and an NBA as a LTS 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11181 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
3e31a6d7df
commit
071d26d603
1 changed files with 271 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 271
      prism/src/explicit/LTSNBAProduct.java

271
prism/src/explicit/LTSNBAProduct.java
View File

@ -0,0 +1,271 @@
//==============================================================================
//
// Copyright (c) 2016-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
//
//------------------------------------------------------------------------------
//
// This file is part of PRISM.
//
// PRISM 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 2 of the License, or
// (at your option) any later version.
//
// PRISM 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 PRISM; if not, write to the Free Software Foundation,
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
//
//==============================================================================
package explicit;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Stack;
import java.util.Vector;
import prism.PrismLog;
import common.IterableBitSet;
import common.IterableStateSet;
import jltl2ba.APElement;
import jltl2dstar.NBA;
import jltl2dstar.NBA_State;
/**
* Construction and storage for the product
* of the underlying labeled transition system
* of a model (i.e., the edge relation defined
* by getSuccessorsIterator()) and a non-deterministic
* Büchi automaton (NBA).
*/
public class LTSNBAProduct extends Product<Model>
{
/** A product state */
private static class ProductState {
/** The model state */
private int modelState;
/** The automaton state */
private int automatonState;
/** Constructor */
public ProductState(int modelState, int automatonState)
{
this.modelState = modelState;
this.automatonState = automatonState;
}
/** Get model state */
public int getModelState()
{
return modelState;
}
/** Get automaton state */
public int getAutomatonState()
{
return automatonState;
}
public String toString() {
return "(" + getModelState() + "," + getAutomatonState() +")";
}
@Override
public int hashCode()
{
final int prime = 31;
int result = 1;
result = prime * result + automatonState;
result = prime * result + modelState;
return result;
}
@Override
public boolean equals(Object obj)
{
if (this == obj)
return true;
if (obj == null)
return false;
if (!(obj instanceof ProductState))
return false;
ProductState other = (ProductState) obj;
if (automatonState != other.automatonState)
return false;
if (modelState != other.modelState)
return false;
return true;
}
}
/** Map state in product -> product state information */
private ArrayList<ProductState> productStates;
/** Accepting Büchi states in the product */
private BitSet acceptingStates;
/** Constructor for storing the product */
private LTSNBAProduct(LTS productModel, Model originalModel, ArrayList<ProductState> productStates, BitSet acceptingStates)
{
super(productModel, originalModel);
this.productStates = productStates;
this.acceptingStates = acceptingStates;
}
@Override
public int getModelState(int productState)
{
return productStates.get(productState).modelState;
}
@Override
public int getAutomatonState(int productState)
{
return productStates.get(productState).automatonState;
}
/** Print the mapping between product state indizes and product states */
public void printStateMapping(PrismLog log)
{
for (int i =0; i < productStates.size(); i++) {
log.println(i + ": " + productStates.get(i) + (acceptingStates.get(i) ? " !":""));
}
}
/** Get the Büchi states for the product */
public BitSet getAcceptingStates()
{
return acceptingStates;
}
/**
* Construct the product.
*
* @param model the model
* @param nba the nondeterministic Büchi automaton
* @param statesOfInterest the states in the model that serve as the starting point for the product
* @param labelBS vector of state sets for the atomic propositions L0, L1, ... in the automaton
*/
public static LTSNBAProduct doProduct(Model model, NBA nba, BitSet statesOfInterest, Vector<BitSet> labelBS)
{
// map state index in product automaton -> ProductState
ArrayList<ProductState> productIdToProductState = new ArrayList<ProductState>();
// map ProductState -> state index in product automaton
HashMap<ProductState, Integer> productStateToProductId = new HashMap<ProductState, Integer>();
// storage for the product model
LTSExplicit productModel = new LTSExplicit();
// the accepting states in the product model
BitSet acceptingStates = new BitSet();
// the stack of product ids that potentially have to be expanded
Stack<Integer> todo = new Stack<Integer>();
// product state ids that have already been expanded
BitSet expanded = new BitSet();
// Note: In contrast to the deterministic automaton product elsewhere in
// PRISM, the automaton step delta(q,l(s)) is done when leaving the product
// state, not when entering. As we are only interested in the infinite behaviour,
// this doesn't change acceptance at all:
//
// <s,q> -> <s',q'> where s->s' in the model and q' in delta(q, l(s))
//
// Thus, the initial states in the product are <s, q_0> for s in the states of interest
// of the model and q_0 the initial state of the NBA.
NBA_State nbaStart = nba.getStartState();
if (nbaStart == null) {
// no start state = rejecting
// to simplify treatment, add a dummy start state
// with no outgoing transitions
nbaStart = nba.newState();
nba.setStartState(nbaStart);
}
// Note: As the NBA currently is guaranteed to have a single initial state,
// the product has exactly one initial product state per model state of interest.
// This allows the use of the "normal" projection back from the product result to
// the original model. For multiple initial NBA states, it would be necessary
// to aggregate the results over all initial NBA states when projecting back to
// the original model.
// for each model state of interest ...
for (int modelState : new IterableStateSet(statesOfInterest, model.getNumStates())) {
// ... construct a product state (modelState, nbaStart)
ProductState p = new ProductState(modelState, nbaStart.getName());
productIdToProductState.add(p);
int id = productModel.addState();
productModel.addInitialState(id);
assert ( id == productIdToProductState.size()-1 );
productStateToProductId.put(p, id);
todo.push(id);
if (nbaStart.isFinal()) {
acceptingStates.set(id);
}
}
while (!todo.isEmpty()) {
int fromId = todo.pop();
if (expanded.get(fromId))
continue;
ProductState from = productIdToProductState.get(fromId);
// construct edge label from the labeling of the model state
APElement label = new APElement(labelBS.size());
for (int ap=0; ap < labelBS.size(); ap++) {
if (labelBS.get(ap).get(from.getModelState())) {
label.set(ap);
} else {
label.clear(ap);
}
}
// the current state in the NBA
NBA_State fromNBA = nba.get(from.getAutomatonState());
// the successors in the NBA for the label corresponding to the model state
BitSet nbaSuccessors = fromNBA.getEdge(label);
// for each successor of the model state ...
for (Iterator<Integer> it = model.getSuccessorsIterator(from.getModelState()); it.hasNext(); ) {
Integer modelTo = it.next();
// ... and NBA successor ...
for (Integer nbaSuccessor : IterableBitSet.getSetBits(nbaSuccessors)) {
// ... construct product state
ProductState successor = new ProductState(modelTo, nbaSuccessor);
Integer successorID = productStateToProductId.get(successor);
if (successorID == null) {
// newly discovered, add as state to the product model
productIdToProductState.add(successor);
successorID = productModel.addState();
assert ( successorID == productIdToProductState.size()-1 );
productStateToProductId.put(successor, successorID);
// mark as todo
todo.push(successorID);
boolean isAccepting = nba.get(nbaSuccessor).isFinal();
if (isAccepting) {
acceptingStates.set(successorID);
}
}
// add the edge
productModel.addEdge(fromId, successorID);
}
// fromId is fully expanded in the product
expanded.set(fromId);
}
}
return new LTSNBAProduct(productModel, model, productIdToProductState, acceptingStates);
}
}
Write Preview
Loading…
Cancel
Save