Linearisability

Documentation

type History pid inv resp = [(pid, Either inv resp)]

linearisable :: Eq pid => (model -> Either inv resp -> model) -> (model -> inv -> resp -> Bool) -> model -> History pid inv resp -> Bool

trace :: (Show model, Show inv, Show resp) => (model -> Either inv resp -> model) -> model -> History ProcessId inv resp -> String

wellformed :: Eq pid => [pid] -> History pid inv resp -> Either (NotSequential pid inv resp) ()