From c20ce96c98fe90d73d3f00949f9e1c53e2b9afce Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 19 Aug 2016 14:01:53 +0000
Subject: [PATCH] param/exact: filter zero probability updates so that they
 don't appear in the model

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11654 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/SymbolicEngine.java | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/prism/src/param/SymbolicEngine.java b/prism/src/param/SymbolicEngine.java
index df55c062..dc314257 100644
--- a/prism/src/param/SymbolicEngine.java
+++ b/prism/src/param/SymbolicEngine.java
@@ -293,6 +293,10 @@ public class SymbolicEngine
 
 			try {
 				Function pFn = modelBuilder.expr2function(functionFactory, p);
+				if (pFn.isZero()) {
+					// function for probability / rate is zero, don't add the corresponding transition
+					continue;
+				}
 				ch.add(pFn, list);
 			} catch (PrismException e) {
 				throw new PrismLangException(e.getMessage());