From 91fc16e4f99bce433c6e33cc040c5222da290933 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 22 Aug 2011 20:50:51 +0000
Subject: [PATCH] Bug fix in PTA model checking (digital clocks): GCD of {0} is
 1.

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

diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index ae868c03..fbee1276 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/prism/src/pta/DigitalClocks.java
@@ -454,6 +454,10 @@ public class DigitalClocks
 			for (int x : ints) {
 				gcd = computeGCD(gcd, x);
 			}
+			if (gcd == 0) {
+				// For the case where clock set is empty or all zeros
+				gcd = 1;
+			}
 			return gcd;
 		}