location.ath

domain Location

module Location {

declare alive: [Location] -> Boolean

# `alive` is a global view of the system. The assumption base describes the
# system at one point in time, and (alive l) says whether location l is alive
# at that point. Time is not modeled, so every observer agrees on this value.
#
# An earlier version took a local view: it asserted that the node executing
# the predicate (`localhost`) is alive, since otherwise it could not execute
# it. In a network partition two nodes can observe different values of
# (alive l), which a single predicate cannot represent, so that view could
# lead to inconsistencies. The global view also means that network partitions
# are not modeled: every alive location is reachable from every other one.
#
# An implementation can only approximate this ground truth, for instance with
# a ping or heartbeat protocol with a timeout, after which a node that has not
# answered is regarded (possibly wrongly) as not alive.
#
# The development asserts no fact about specific locations. Examples and tests
# declare their own alive and dead locations.

} # close module Location

open Location