Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 9 additions & 26 deletions prism/src/explicit/DTMCEmbeddedSimple.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
package explicit;

import java.util.*;
import java.util.AbstractMap.SimpleImmutableEntry;
import java.util.Map.Entry;

import explicit.rewards.MCRewards;
Expand Down Expand Up @@ -208,12 +209,11 @@ public Iterator<Entry<Integer,Double>> getTransitionsIterator(int s)
{
if (exitRates[s] == 0) {
// return prob-1 self-loop
return Collections.singletonMap(s, 1.0).entrySet().iterator();
return DiracDistribution.iterator(s);
} else {
final Iterator<Entry<Integer,Double>> ctmcIterator = ctmc.getTransitionsIterator(s);

Iterator<Entry<Integer,Double>> ctmcIterator = ctmc.getTransitionsIterator(s);
// return iterator over entries, with probabilities divided by exitRates[s]
final double er = exitRates[s];
double er = exitRates[s];
return new Iterator<Entry<Integer,Double>>() {
@Override
public boolean hasNext()
Expand All @@ -224,27 +224,10 @@ public boolean hasNext()
@Override
public Entry<Integer, Double> next()
{
final Entry<Integer, Double> ctmcEntry = ctmcIterator.next();

return new Entry<Integer, Double>() {
@Override
public Integer getKey()
{
return ctmcEntry.getKey();
}

@Override
public Double getValue()
{
return ctmcEntry.getValue() / er;
}

@Override
public Double setValue(Double value)
{
throw new UnsupportedOperationException();
}
};
Entry<Integer, Double> transition = ctmcIterator.next();
Integer state = transition.getKey();
double probability = transition.getValue() / er;
return new SimpleImmutableEntry<>(state, probability);
}
};
}
Expand All @@ -253,7 +236,7 @@ public Double setValue(Double value)
@Override
public void forEachTransition(int s, TransitionConsumer c)
{
final double er = exitRates[s];
double er = exitRates[s];
if (er == 0) {
// exit rate = 0 -> prob 1 self loop
c.accept(s, s, 1.0);
Expand Down
81 changes: 81 additions & 0 deletions prism/src/explicit/DiracDistribution.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
//==============================================================================
//
// Copyright (c) 2019-
// Authors:
// * Steffen Maercker <steffen.maercker@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.Iterator;
import java.util.Map;
import java.util.Map.Entry;

import common.iterable.SingletonIterator;

public class DiracDistribution implements Iterable<Entry<Integer, Double>>
{
private final Entry<Integer, Double> transition;

public DiracDistribution(final int state)
{
this.transition = new Transition(state);
}

public Iterator<Entry<Integer, Double>> iterator()
{
return new SingletonIterator.Of<>(transition);
}

public static Iterator<Entry<Integer, Double>> iterator(final int state)
{
return new SingletonIterator.Of<>((Entry<Integer, Double>) new Transition(state));
}

public static class Transition implements Map.Entry<Integer, Double>
{
private final Integer state;

public Transition(final int state)
{
this.state = state;
}

@Override
public Integer getKey()
{
return state;
}

@Override
public Double getValue()
{
return 1.0;
}

@Override
public Double setValue(final Double value)
{
throw new UnsupportedOperationException("immutable entry");
}
}
}