< Marriage AutoProof Code Repository Observer >

Master clock

Category: Invariant

Source: MPC'04 / SC'14

Description

Master clock has two methods: tick (which increments time) and reset (which resets time to zero). Slave clock stores a cache, which should be no greater than master's current time. The slaves should be synchronized as rarely as possible, i.e. only after a reset.

download source

Code