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

Simulator updates, including local nondet (untested). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1982 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
3e49feef72
commit
cd36ad544f
2 changed files with 130 additions and 141 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. 64
      prism/src/simulator/ChoiceListFlexi.java
  2. 207
      prism/src/simulator/Updater.java

64
prism/src/simulator/ChoiceListFlexi.java
View File

@ -34,18 +34,21 @@ import prism.PrismLangException;
public class ChoiceListFlexi implements Choice
{
// TODO: need mult actions
//protected String action;
// Module/action info, encoded as an integer.
// For an independent (non-synchronous) choice, this is -i,
// where i is the 1-indexed module index.
// For a synchronous choice, this is the 1-indexed action index.
protected int moduleOrActionIndex;
// List of multiple targets and associated info
// Size of list is stored implicitly in target.length
// TODO: convert to arrays?
protected List<List<Update>> updates;
protected List<Double> probability;
protected List<Command> command;
/**
* Create empty choice.
*/
public ChoiceListFlexi()
{
updates = new ArrayList<List<Update>>();
@ -55,19 +58,32 @@ public class ChoiceListFlexi implements Choice
// Set methods
/**
* Set the module/action for this choice, encoded as an integer
* (-i for independent in ith module, i for synchronous on ith action)
* (in both cases, modules/actions are 1-indexed)
*/
public void setModuleOrActionIndex(int moduleOrActionIndex)
{
this.moduleOrActionIndex = moduleOrActionIndex;
}
public void add(String action, double probability, List<Update> ups, Command command)
/**
* Add a transition to this choice.
* @param probability Probability (or rate) of the transition
* @param ups List of Update objects defining transition
* @param command Corresponding Command object
*/
public void add(double probability, List<Update> ups, Command command)
{
//this.action = action;
this.updates.add(ups);
this.probability.add(probability);
this.command.add(command);
}
/**
* Scale probability/rate of all transitions, multiplying by d.
*/
public void scaleProbabilitiesBy(double d)
{
int i, n;
@ -77,6 +93,9 @@ public class ChoiceListFlexi implements Choice
}
}
/**
* Modify this choice, constructing product of it with another.
*/
public void productWith(ChoiceListFlexi ch)
{
List<Update> list;
@ -98,7 +117,7 @@ public class ChoiceListFlexi implements Choice
for (Update u : ch.updates.get(i)) {
list.add(u);
}
add("?", pi * getProbability(j), list, null);
add(pi * getProbability(j), list, null);
}
}
// Modify elements of current choice to get (0,j) elements of product
@ -113,11 +132,20 @@ public class ChoiceListFlexi implements Choice
// Get methods
/**
* Get the module/action for this choice, as an integer index
* (-i for independent in ith module, i for synchronous on ith action)
* (in both cases, modules/actions are 1-indexed)
*/
public int getModuleOrActionIndex()
{
return moduleOrActionIndex;
}
/**
* Get the module/action for this choice, as a string
* (form is "module" or "[action]")
*/
public String getModuleOrAction()
{
Update u = updates.get(0).get(0);
@ -128,11 +156,17 @@ public class ChoiceListFlexi implements Choice
return "[" + c.getSynch() + "]";
}
/**
* Get the number of transitions in this choice.
*/
public int size()
{
return probability.size();
}
/**
* Get the updates of the ith transition, as a string.
*/
public String getUpdateString(int i)
{
String s = "(";
@ -142,6 +176,9 @@ public class ChoiceListFlexi implements Choice
return s;
}
/**
* Compute the target for the ith transition, based on a current state.
*/
public State computeTarget(int i, State oldState) throws PrismLangException
{
if (i < 0 || i >= size())
@ -152,6 +189,9 @@ public class ChoiceListFlexi implements Choice
return newState;
}
/**
* Compute the target for the ith transition, based on a current state, store in a State.
*/
public void computeTarget(int i, State oldState, State newState) throws PrismLangException
{
if (i < 0 || i >= size())
@ -170,11 +210,6 @@ public class ChoiceListFlexi implements Choice
computeTarget(0, oldState, newState);
}
public double getProbability()
{
return getProbability(0);
}
public double getProbability(int i)
{
if (i < 0 || i >= size())
@ -183,6 +218,11 @@ public class ChoiceListFlexi implements Choice
return probability.get(i);
}
public double getProbability()
{
return getProbability(0);
}
public double getProbabilitySum()
{
double sum = 0.0;

207
prism/src/simulator/Updater.java
View File

@ -50,23 +50,22 @@ public class Updater
protected int numRewardStructs;
// Temporary storage:
// Element i,j of updateLists is a list of the updates from module i labelled with action j
// (where j=0 denotes independent, otherwise 1-indexed action label)
protected List<List<List<Updates>>> updateLists;
// Bit j of enabledSynchs is set iff action j is currently enabled
// (where j=0 denotes independent, otherwise 1-indexed action label)
protected BitSet enabledSynchs;
// Element j of enabledSynchs is BitSet showing modules which enable action j
// Element j of enabledModules is a BitSet showing modules which enable action j
// (where j=0 denotes independent, otherwise 1-indexed action label)
protected BitSet enabledModules[];
// TODO: apply optimiseForFast or assume called?
public Updater(SimulatorEngine simulator, ModulesFile modulesFile)
{
int i, j;
String s;
// Get info from simulator/model
this.simulator = simulator;
prism = simulator.getPrism();
@ -76,7 +75,7 @@ public class Updater
synchs = modulesFile.getSynchs();
numSynchs = synchs.size();
numRewardStructs = modulesFile.getNumRewardStructs();
// Compute count of number of modules using each synch action
synchModuleCounts = new int[numSynchs];
for (j = 0; j < numSynchs; j++) {
@ -87,7 +86,7 @@ public class Updater
synchModuleCounts[j]++;
}
}
// Build lists/bitsets for later use
updateLists = new ArrayList<List<List<Updates>>>(numModules);
for (i = 0; i < numModules; i++) {
@ -110,13 +109,9 @@ public class Updater
*/
public void calculateTransitions(State state, TransitionList transitionList) throws PrismException
{
Module module;
ChoiceListFlexi prod;
int i, j, n, count, n2, n3;
double p;
List<ChoiceListFlexi> chs;
int i, j, k, l, n, count;
//System.out.println("Synchs: " + synchs);
//System.out.println("Calc updates for " + state);
// Clear lists/bitsets
transitionList.clear();
for (i = 0; i < numModules; i++) {
@ -128,122 +123,95 @@ public class Updater
for (i = 0; i < numSynchs + 1; i++) {
enabledModules[i].clear();
}
// Calculate the available updates for each module/action
// (update information in updateLists, enabledSynchs and enabledModules)
for (i = 0; i < numModules; i++) {
calculateUpdatesForModule(i, state);
}
//System.out.println("updateLists: " + updateLists);
// Combination of updates depends on model type
/*switch (modelType) {
case DTMC:
case CTMC:*/
n = 0;
// Independent choices for each (enabled) module
for (i = enabledModules[0].nextSetBit(0); i >= 0; i = enabledModules[0].nextSetBit(i + 1)) {
for (Updates ups : updateLists.get(i).get(0)) {
/*processUpdatesAndAddToSum(ups, state, ch);
n++;*/
transitionList.add(processUpdatesAndCreateNewChoice(-(i + 1), ups, state));
}
// Add independent transitions for each (enabled) module to list
for (i = enabledModules[0].nextSetBit(0); i >= 0; i = enabledModules[0].nextSetBit(i + 1)) {
for (Updates ups : updateLists.get(i).get(0)) {
transitionList.add(processUpdatesAndCreateNewChoice(-(i + 1), ups, state));
}
// Add synchronous transitions to list
for (i = enabledSynchs.nextSetBit(1); i >= 0; i = enabledSynchs.nextSetBit(i + 1)) {
// Check counts to see if this action is blocked by some module
if (enabledModules[i].cardinality() < synchModuleCounts[i - 1])
continue;
// If not, proceed...
prod = null;
for (j = enabledModules[i].nextSetBit(0); j >= 0; j = enabledModules[i].nextSetBit(j + 1)) {
count = updateLists.get(j).get(i).size();
// Case where there is 1 choice
if (count == 1) {
// Case where this is the first Updates added
if (prod == null) {
for (Updates ups : updateLists.get(j).get(i)) {
prod = processUpdatesAndCreateNewChoice(i, ups, state);
}
} else {
processUpdatesAndAddToProduct(updateLists.get(j).get(i).get(0), state, prod);
}
}
// Add synchronous transitions to list
chs = new ArrayList<ChoiceListFlexi>();
for (i = enabledSynchs.nextSetBit(1); i >= 0; i = enabledSynchs.nextSetBit(i + 1)) {
chs.clear();
// Check counts to see if this action is blocked by some module
if (enabledModules[i].cardinality() < synchModuleCounts[i - 1])
continue;
// If not, proceed...
for (j = enabledModules[i].nextSetBit(0); j >= 0; j = enabledModules[i].nextSetBit(j + 1)) {
count = updateLists.get(j).get(i).size();
// Case where there is only 1 Updates for this module
if (count == 1) {
Updates ups = updateLists.get(j).get(i).get(0);
// Case where this is the first Choice created
if (chs.size() == 0) {
chs.add(processUpdatesAndCreateNewChoice(i, ups, state));
}
// Case where there are multiple choices
// Case where there are existing Choices
else {
// TODO
throw new PrismLangException("Don't handle local nondet yet");
// Product with all existing choices
for (ChoiceListFlexi ch : chs) {
processUpdatesAndAddToProduct(ups, state, ch);
}
}
//System.out.println("prod" + j + ": " + prod);
}
transitionList.add(prod);
n++;
}
/*if (n > 1)
ch.scaleProbabilitiesBy(1.0 / n);
transitionList.add(ch);*/
//break;
//case MDP:
/*
// Add independent transitions to list
for (i = 0; i < numModules; i++) {
for (Updates ups : updateLists.get(i).get(0)) {
transitionList.add(calculateTransitionsForUpdates(ups, state));
}
}
// Add synchronous transitions to list
for (i = 0; i < numSynchs; i++) {
prod = new ArrayList<Updates>();
for (j = 0; j < numModules; j++) {
// Skip modules not using this action
if (!modulesFile.getModule(j).usesSynch(synchs.get(i)))
continue;
// Case where module blocks
if (updateLists.get(j).get(i).size() == 0) {
prod.clear();
break;
}
// Case where this is the first Updates added
if (prod.isEmpty()) {
// Case where there are multiple Updates (i.e. local nondeterminism)
else {
// Case where there are no existing choices
if (chs.size() == 0) {
for (Updates ups : updateLists.get(j).get(i)) {
// TODO: avoid so much copying for efficiency?
prod.add((Updates) ups.deepCopy());
chs.add(processUpdatesAndCreateNewChoice(i, ups, state));
}
}
// Case where there is 1 choice
else if (updateLists.get(j).get(i).size() == 1) {
}
// Case where there are multiple choices
// Case where there are existing Choices
else {
// TODO
//for (Choice tr : choiceLists.get(j).get(i)) {
// Duplicate (count-1 copies of) current Choice list
n = chs.size();
for (k = 0; k < count - 1; k++)
for (l = 0; l < n; l++)
chs.add(chs.get(l));
// Products with existing choices
for (k = 0; k < count; k++) {
Updates ups = updateLists.get(j).get(i).get(k);
for (l = 0; l < n; l++)
processUpdatesAndAddToProduct(ups, state, chs.get(k * n + l));
}
}
}
for (Updates ups : prod) {
transitionList.add(calculateTransitionsForUpdates(ups, state));
}
}*/
/*break;
default:
throw new PrismException("Unhandled model type \"" + modelType + "\"");
}*/
// For DTMCs, need to randomise
}
// Add all new choices to transition list
for (ChoiceListFlexi ch : chs) {
transitionList.add(ch);
}
}
//System.out.println(transitionList);
}
// Private helpers
/**
* Create a new Choice object (currently ChoiceListFlexi) based on an Updates object
* and a (global) state. If appropriate, check probabilities sum to 1 too.
* @param moduleOrActionIndex Module/action for the choice, encoded as an integer (see Choice)
* @param ups The Updates object
* @param state Global state
*/
private ChoiceListFlexi processUpdatesAndCreateNewChoice(int moduleOrActionIndex, Updates ups, State state) throws PrismLangException
{
// TODO: use sum function?
ChoiceListFlexi ch;
List<Update> list;
int i, n;
double p, sum;
// Create choice and add all info
ch = new ChoiceListFlexi();
ch.setModuleOrActionIndex(moduleOrActionIndex);
n = ups.getNumUpdates();
@ -253,7 +221,7 @@ public class Updater
sum += p;
list = new ArrayList<Update>();
list.add(ups.getUpdate(i));
ch.add("", p, list, ups.getParent());
ch.add(p, list, ups.getParent());
}
// Check distribution sums to 1 (if required)
if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) {
@ -263,28 +231,14 @@ public class Updater
return ch;
}
private void processUpdatesAndAddToSum(Updates ups, State state, ChoiceListFlexi ch) throws PrismLangException
{
List<Update> list;
int i, n;
double p, sum;
n = ups.getNumUpdates();
sum = 0;
for (i = 0; i < n; i++) {
p = ups.getProbabilityInState(i, state);
sum += p;
list = new ArrayList<Update>();
list.add(ups.getUpdate(i));
ch.add("", p, list, ups.getParent());
}
// Check distribution sums to 1 (if required)
if (modelType.choicesSumToOne() && Math.abs(sum - 1) > prism.getSumRoundOff()) {
throw new PrismLangException("Probabilities sum to " + sum + " in state " + state);
}
}
/**
* Create a new Choice object (currently ChoiceListFlexi) based on the product
* of an existing ChoiceListFlexi and an Updates object, for some (global) state.
* If appropriate, check probabilities sum to 1 too.
* @param ups The Updates object
* @param state Global state
* @param ch The existing Choices object
*/
private void processUpdatesAndAddToProduct(Updates ups, State state, ChoiceListFlexi ch) throws PrismLangException
{
// Create new choice (action index is 0 - not needed)
@ -293,22 +247,17 @@ public class Updater
ch.productWith(chNew);
}
// Model exploration methods (e.g. for simulation)
/**
* Determine the enabled updates for the 'm'th module from (global) state 'state'.
* Update information in ... TODO
* Update information in updateLists, enabledSynchs and enabledModules.
* @param m The module index
* @param state State from which to explore
* @param ...
* TODO
*/
private void calculateUpdatesForModule(int m, State state) throws PrismLangException
{
Module module;
Command command;
int i, j, n;
String s;
module = modulesFile.getModule(m);
n = module.getNumCommands();

Write Preview
Loading…
Cancel
Save