Browse Source

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
master
Dave Parker 15 years ago
parent
commit
91fc16e4f9
  1. 4
      prism/src/pta/DigitalClocks.java

4
prism/src/pta/DigitalClocks.java

@ -454,6 +454,10 @@ public class DigitalClocks
for (int x : ints) { for (int x : ints) {
gcd = computeGCD(gcd, x); gcd = computeGCD(gcd, x);
} }
if (gcd == 0) {
// For the case where clock set is empty or all zeros
gcd = 1;
}
return gcd; return gcd;
} }

Loading…
Cancel
Save