Yices 1.0.38 Counterexample: ======================== Path ======================== Step 0: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 0 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 60 alarm3Sounding = false alarm3StartTime = 0 alarm3TimeInCycle = 0 alarm3Volume = 0 globalTime = 0 maxNextTime = 60 ------------------------ Step 1: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 23/160 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 60 alarm3Sounding = false alarm3StartTime = 0 alarm3TimeInCycle = 23/160 alarm3Volume = 0 globalTime = 23/160 maxNextTime = 60 ------------------------ Step 2: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 1885/32 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 60 alarm3Sounding = false alarm3StartTime = 0 alarm3TimeInCycle = 1885/32 alarm3Volume = 0 globalTime = 1885/32 maxNextTime = 60 ------------------------ Step 3: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 277 alarm2Masked = false alarm2NextTime = 4731/80 alarm2Sounding = true alarm2StartTime = 4719/80 alarm2TimeInCycle = 0 alarm2Volume = 60 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 60 alarm3Sounding = false alarm3StartTime = 0 alarm3TimeInCycle = 4719/80 alarm3Volume = 0 globalTime = 4719/80 maxNextTime = 4731/80 ------------------------ Step 4: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = true alarm2NextTime = 947/16 alarm2Sounding = true alarm2StartTime = 4719/80 alarm2TimeInCycle = 3/20 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 524 alarm3Masked = false alarm3NextTime = 4747/80 alarm3Sounding = true alarm3StartTime = 4731/80 alarm3TimeInCycle = 0 alarm3Volume = 85 globalTime = 4731/80 maxNextTime = 947/16 ------------------------ Step 5: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 277 alarm2Masked = false alarm2NextTime = 4747/80 alarm2Sounding = true alarm2StartTime = 4719/80 alarm2TimeInCycle = 1/5 alarm2Volume = 60 alarm3CycleTime = 19/40 alarm3Frequency = 524 alarm3Masked = false alarm3NextTime = 4747/80 alarm3Sounding = true alarm3StartTime = 4731/80 alarm3TimeInCycle = 1/20 alarm3Volume = 85 globalTime = 947/16 maxNextTime = 4747/80 ------------------------ Step 6: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 4747/80 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 4753/80 alarm3Sounding = true alarm3StartTime = 4731/80 alarm3TimeInCycle = 1/5 alarm3Volume = 0 globalTime = 4747/80 maxNextTime = 4753/80 ------------------------ Step 7: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 4753/80 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 294 alarm3Masked = false alarm3NextTime = 4769/80 alarm3Sounding = true alarm3StartTime = 4731/80 alarm3TimeInCycle = 11/40 alarm3Volume = 85 globalTime = 4753/80 maxNextTime = 4769/80 ------------------------ Step 8: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = false alarm2NextTime = 60 alarm2Sounding = false alarm2StartTime = 0 alarm2TimeInCycle = 4769/80 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = false alarm3NextTime = 60 alarm3Sounding = false alarm3StartTime = 0 alarm3TimeInCycle = 4769/80 alarm3Volume = 0 globalTime = 4769/80 maxNextTime = 60 ------------------------ Step 9: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 277 alarm2Masked = false alarm2NextTime = 9623/160 alarm2Sounding = true alarm2StartTime = 9599/160 alarm2TimeInCycle = 0 alarm2Volume = 60 alarm3CycleTime = 19/40 alarm3Frequency = 524 alarm3Masked = false alarm3NextTime = 9631/160 alarm3Sounding = true alarm3StartTime = 9599/160 alarm3TimeInCycle = 0 alarm3Volume = 85 globalTime = 9599/160 maxNextTime = 9623/160 ------------------------ Step 10: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 0 alarm2Masked = true alarm2NextTime = 9631/160 alarm2Sounding = true alarm2StartTime = 9599/160 alarm2TimeInCycle = 3/20 alarm2Volume = 0 alarm3CycleTime = 19/40 alarm3Frequency = 524 alarm3Masked = false alarm3NextTime = 9631/160 alarm3Sounding = true alarm3StartTime = 9599/160 alarm3TimeInCycle = 3/20 alarm3Volume = 85 globalTime = 9623/160 maxNextTime = 9631/160 ------------------------ Step 11: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 277 alarm2Masked = false alarm2NextTime = 1931/32 alarm2Sounding = true alarm2StartTime = 9599/160 alarm2TimeInCycle = 1/5 alarm2Volume = 60 alarm3CycleTime = 19/40 alarm3Frequency = 0 alarm3Masked = true alarm3NextTime = 9643/160 alarm3Sounding = true alarm3StartTime = 9599/160 alarm3TimeInCycle = 1/5 alarm3Volume = 0 globalTime = 9631/160 maxNextTime = 9643/160 ------------------------ Step 12: --- System Variables (assignments) --- alarm2CycleTime = 7/20 alarm2Frequency = 277 alarm2Masked = true alarm2NextTime = 1931/32 alarm2Sounding = true alarm2StartTime = 9599/160 alarm2TimeInCycle = 11/40 alarm2Volume = 60 alarm3CycleTime = 19/40 alarm3Frequency = 294 alarm3Masked = false alarm3NextTime = 1935/32 alarm3Sounding = true alarm3StartTime = 9599/160 alarm3TimeInCycle = 11/40 alarm3Volume = 85 globalTime = 9643/160 maxNextTime = 1931/32