Nicolas Trangez NicolasT

An e-mail I sent to the authors of the PaxosLease paper back in the day. One of them replied explaining how in their actual implementation of the protocol (http://github.com/scalien/keyspace/tree/master/src/Framework/PaxosLease) they added phase separation/tracking (bool preparing and bool proposing), which would indeed solve the issue with the protocol outlined in the paper as explained in the e-mail.

	module Functor = struct
	module type S = sig
	type 'a t

	val map : ('a -> 'b) -> 'a t -> 'b t
	end

	module type API = sig
	include S

	module Main (main) where

	import Data.SBV

	raadsel :: Symbolic SBool
	raadsel = do
	vars@[s, e, n, d, m, o, r, y] <- sIntegers ["s", "e", "n", "d", "m", "o", "r", "y"]

	-- Helper, maakt bvb. (100 * a + 10 * b + c) uit [a, b, c]
	let woord w = sum (zipWith () (reverse w) (iterate ( 10) 1))

	import sys
	import fcntl
	import socket
	import struct

	'''
	#include <stdio.h>
	#include <net/if.h>
	#include <netinet/in.h>
	#include <sys/ioctl.h>

	%global provider github
	%global provider_tld com
	%global project projectcalico
	%global repo cni-plugin
	%global provider_prefix %{provider}.%{provider_tld}/%{project}/%{repo}

	%ifarch x86_64
	%global built_arch amd64
	%global calico_sha256 5736d46dc8f3d17eafd1d7874c49457244b698d5fccf726066c60c136ac5a318
	%global calico_ipam_sha256 ae32622d5c904e216cd914031e560e481c9ea9c213153172d0eacabadbb5e984

	-- See below
	-- {-# LANGUAGE AllowAmbiguousTypes #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE RebindableSyntax #-}
	{-# LANGUAGE ScopedTypeVariables #-}

	import Prelude hiding ((>>=), (>>), return)
	import qualified Prelude as P

	import Data.Functor.Identity (Identity, runIdentity)

	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE ViewPatterns #-}

	module Main where

	import Data.Monoid
	import Control.Lens

	__pycache__/
	.pytest_cache/