-- CONCRETE WORLD AND INDIVIDUAL OPERATIONS ON CONCRETE PURSES

module mondex/c
open mondex/a

-- We need a total order for the sequences ("time"). Actually in the Z
-- specification, integers are used, but for this purpose only their order
-- properties are used.

open util/ordering [SEQNO] as seqord

sig SEQNO {}


-- Concrete purse status : an enumeration of the possible status of a
-- concrete purse.

abstract sig STATUS {}
one sig eaFrom, eaTo, epr, epv, epa extends STATUS {}


-- When a purse initiates a transfer process, it queries information about
-- the other purse, and the sequence number to have the process
-- "synchronized".

sig CounterPartyDetails {
	name : NAME,
	value : set Coin,
	next : SEQNO
}


-- Concrete transfer details. Extends the Abstract transfer details with
-- the two time indications of the involved purses at the beginning of the
-- transfer.

sig PayDetails extends TransferDetails {
	fromSeqNo, toSeqNo : SEQNO
} {
	from not = to
}

-- Clear code. The Z specification requires that there exist a set CLEAR of
-- clear codes and an injective function from P(PayDetails) to CLEAR. It
-- should actually work like a "hashing" function to check the
-- identification of sets of PayDetails without carrying the whole
-- information. This injective function, image, is represented here as
-- imageRecip, that is in the opposite way.

sig CLEAR {
	image_recip : set PayDetails
}

fact image_def {
	no disj c, c' : CLEAR | c.image_recip = c'.image_recip
}

fun image (e : set PayDetails) : CLEAR {
	{c : CLEAR | c.image_recip = e}
}


-- OPERATION MESSAGES

abstract sig MESSAGE {}

sig startFrom extends MESSAGE {details: CounterPartyDetails}
sig startTo extends MESSAGE {details : CounterPartyDetails}
one sig readExceptionLog extends MESSAGE {}
sig req extends MESSAGE {details: PayDetails}
sig val extends MESSAGE {details: PayDetails}
sig ack extends MESSAGE {details : PayDetails}
sig exceptionLogResult extends MESSAGE  {
	name : NAME,
	details: PayDetails
}
sig exceptionLogClear extends MESSAGE {
	name : NAME,
	clear : CLEAR
}
one sig bottom extends MESSAGE {}



-- CONCRETE PURSE

-- with constraints required by the Z spec, and some other constraints I
-- think the spec has forgotten.  exLog is the "private archive" of the
-- purse, logging the failed transactions involving the purse. But the
-- LogClear operations allow a purse to log them into the "public archive"
-- and clear its private archive. pdAuth is the current transaction in
-- progress involving the purse.

sig ConPurse {
	balance : set Coin,
	exLog : set PayDetails,
	name : NAME,
	nextSeqNo : SEQNO,
	pdAuth : PayDetails,
	status : STATUS
} {
	all pd : PayDetails | pd in exLog implies name in pd.from+pd.to

	status in epr implies {
		name = pdAuth.from
		pdAuth.value in balance
		seqord/lt (pdAuth.fromSeqNo, nextSeqNo)
	}
	status in epv implies {
		name = pdAuth.to -- ADDED
		seqord/lt (pdAuth.toSeqNo, nextSeqNo)
	}

	status in epa implies {
		-- rajoute a la main
		name = pdAuth.from -- ADDED
		seqord/lt (pdAuth.fromSeqNo, nextSeqNo)
	}

-- this constraint is due to the coin representation of values. It is
-- equivalent to forbidding common coins between balance and lost values.
	no exLog.value & balance

}



-- INDIVIDUAL PURSE OPERATIONS

-- The following predicate logs the current transaction in progress into
-- the private archive, considering it lost, if the purse is in a critical
-- status.

pred LogIfNecessary (p, p' : ConPurse) {
	p'.exLog = p.exLog + if p.status in epv + epa then p.pdAuth else none
}

-- The Xi predicates indicate which fields of a purse are left unchanged
-- through an individual operation. 

-- Increase : this operation increases the time 

pred XiConPurseIncrease (p, p' : ConPurse) {
	p.balance = p'.balance
	p.exLog = p'.exLog
	p.name = p'.name
	p.pdAuth = p'.pdAuth
	p.status = p'.status
}

pred IncreasePurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	XiConPurseIncrease (p, p')
	seqord/gte (p'.nextSeqNo, p.nextSeqNo)
	m_out = bottom
}

-- Abort : this operation aborts the current operation in progress
-- involving the purse.

pred XiConPurseAbort (p, p' : ConPurse) {
	p.balance = p'.balance
	p.name = p'.name
}

pred AbortPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	p'.status = eaFrom
	seqord/gte (p'.nextSeqNo, p.nextSeqNo)
	XiConPurseAbort (p, p')
	LogIfNecessary (p, p')
}

-- Xi predicates for other operations

pred XiConPurseStart (p, p' : ConPurse) {
	p.balance = p'.balance
	p.exLog = p'.exLog
	p.name = p'.name	
}

pred XiConPurseReq (p, p' : ConPurse) {
	p.exLog = p'.exLog
	p.name = p'.name
	p.nextSeqNo = p'.nextSeqNo
	p.pdAuth = p'.pdAuth
}

pred XiConPurseVal (p, p' : ConPurse) {
	XiConPurseReq (p, p')
}

pred XiConPurseAck (p, p' : ConPurse) {
	p.balance = p'.balance
	p.exLog = p'.exLog
	p.name = p'.name
	p.nextSeqNo = p'.nextSeqNo
}

-- StartFrom : the paying purse identifies itself. Actually, it receives
-- the StartFrom message, requesting it to check its constraints (time
-- constraints and sufficient funds property) and change its status to
-- expecting Req message.

pred ValidStartFrom (p : ConPurse, m_in : MESSAGE, cpd : CounterPartyDetails) {
	m_in in startFrom
	cpd = (m_in :> startFrom).details
	cpd.name not = p.name
	cpd.value in p.balance
}

pred StartFromPurseEafromOkay (p, p' : ConPurse, m_in, m_out : MESSAGE, cpd : CounterPartyDetails) {
	ValidStartFrom (p, m_in, cpd)
	p.status = eaFrom
	XiConPurseStart (p, p')
	seqord/gt (p'.nextSeqNo, p.nextSeqNo)
	p'.pdAuth.from = p.name
	p'.pdAuth.to = cpd.name
	p'.pdAuth.value = cpd.value
	p'.pdAuth.fromSeqNo = p.nextSeqNo
	p'.pdAuth.toSeqNo = cpd.next
	p'.status = epr
	m_out = bottom
}

pred StartFromPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	some p'' : ConPurse {
		AbortPurseOkay (p, p'', m_in, m_out)
		some cpd : CounterPartyDetails | StartFromPurseEafromOkay (p'', p', m_in, m_out, cpd)
	}
}

-- StartTo : the payed-to purse identifies itself. Actually, it receives a
-- StartTo message requesting it to send a Req message and change its
-- status to expecting Val message.

pred ValidStartTo (p : ConPurse, m_in : MESSAGE, cpd : CounterPartyDetails) {
	m_in in startTo
	cpd = (m_in :> startTo).details
	cpd.name not = p.name
}

pred StartToPurseEafromOkay (p, p' : ConPurse, m_in, m_out : MESSAGE, cpd : CounterPartyDetails) {
	ValidStartTo (p, m_in, cpd)
	p.status = eaFrom
	XiConPurseStart (p, p')
	seqord/gt (p'.nextSeqNo, p.nextSeqNo)
	p'.pdAuth.to = p.name
	p'.pdAuth.from = cpd.name
	p'.pdAuth.value = cpd.value
	p'.pdAuth.toSeqNo = p.nextSeqNo
	p'.pdAuth.fromSeqNo = cpd.next
	p'.status = epv
	m_out in req
	(m_out :> req).details = p'.pdAuth	
}

pred StartToPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	some p'' : ConPurse {
		AbortPurseOkay (p, p'', m_in, m_out)
		some cpd : CounterPartyDetails | StartToPurseEafromOkay (p'', p', m_in, m_out, cpd)
	}
}

-- Req : the paying purse receives the Req message from the payed-to
-- purse. It decreases its balance and sends a Val message, and changes its
-- status to expecting the Ack message from the payed-to purse.

pred AuthenticReqMessage (p : ConPurse, m_in : MESSAGE) {
	m_in in req
	(m_in :> req).details = p.pdAuth
}

pred ReqPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	AuthenticReqMessage (p, m_in)
	p.status = epr
	XiConPurseReq (p, p')
	p'.balance = p.balance - p.pdAuth.value
	p'.status = epa
	m_out in val
	(m_out :> val).details = p.pdAuth
}

-- Val : the payed-to purse receives the Val message from the paying
-- purse. It increases its balance and sends a Ack message.

pred AuthenticValMessage (p : ConPurse, m_in : MESSAGE) {
	m_in in val
	(m_in :> val).details = p.pdAuth
}

pred ValPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	AuthenticValMessage (p, m_in)
	p.status = epv
	XiConPurseVal (p, p')
	p'.balance = p.balance + p.pdAuth.value
	p'.status = eaTo
	m_out in ack
	(m_out :> ack).details = p.pdAuth
}

-- Ack : the paying purse receives the Ack message, that means that the
-- value has been successfully transferred.

pred AuthenticAckMessage (p : ConPurse, m_in : MESSAGE) {
	m_in in ack
	(m_in :> ack).details = p.pdAuth
}

pred AckPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	AuthenticAckMessage (p, m_in)
	p.status = epa
	XiConPurseAck (p, p')
	p'.status = eaFrom
	m_out = bottom
}

-- Exception logging

-- ReadExceptionLog : a purse receives the ReadExceptionLog message. Then,
-- it sends back the contents of its private archive it wants to log to
-- the public archive.

pred ReadExceptionLogPurseEafromOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	p = p'  -- XiConPurse ??
	m_in = readExceptionLog
	p.status = eaFrom
	m_out in bottom + exceptionLogResult
	m_out in exceptionLogResult implies {
		(m_out :> exceptionLogResult).name = p.name
		(m_out :> exceptionLogResult).details in p'.exLog
	}
}

pred ReadExceptionLogPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	some p'' : ConPurse {
		AbortPurseOkay (p, p'',m_in, m_out)
		ReadExceptionLogPurseEafromOkay (p'', p', m_in, m_out)
	}
}

-- ClearExceptionLog : a purse receives a ClearExceptionLog message with a
-- clear ("hash") code. If the code matches the clear ("hash") value of the
-- contents of its private archive, then the purse clears it.

pred XiConPurseClear (p, p' : ConPurse) {
	p.balance = p'.balance
	p.name = p'.name
	p.pdAuth = p'.pdAuth
	p.status = p'.status
	p.nextSeqNo = p'.nextSeqNo	
}

pred ClearExceptionLogPurseEafromOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	some p.exLog
	m_in in exceptionLogClear
	(m_in :> exceptionLogClear).name = p.name
-- faux :
--	(m_in :> exceptionLogClear).clear = p.exLog.~image_recip
	(m_in :> exceptionLogClear).clear.image_recip = p.exLog
	p.status = eaFrom
	XiConPurseClear (p, p')
	no p'.exLog
	m_out = bottom
}

pred ClearExceptionLogPurseOkay (p, p' : ConPurse, m_in, m_out : MESSAGE) {
	some p'' : ConPurse {
		AbortPurseOkay (p, p'', m_in, m_out)
		ClearExceptionLogPurseEafromOkay (p'', p', m_in, m_out)
	}
}



-- CONCRETE WORLD

-- Logbook : models a public archive, tagging each item of transfer
-- information with the names of the involved purses.

sig Logbook { log : NAME -> PayDetails } {
	all n : NAME, pd : PayDetails | n -> pd in log implies n in pd.from + pd.to

-- I added the following constraint over values of different logged transfer
-- details. They must be disjoint sets of coins, as each logged transfer
-- represents a lost transfer : a coin cannot be lost more than once.

	no disj pd1, pd2 : PayDetails {
		pd1 + pd2 in NAME.log
		some pd1.value & pd2.value
	}

}

-- Unicity constraint

fact {
	no disj l, l' : Logbook | l.log = l'.log
}

-- UNUSED
one sig AllLogs extends Logbook {} {
	all n : NAME, pd : PayDetails | n in pd.from + pd.to implies pd in n.log
}

-- This defines the constraints that hold for a Concrete world. Instead of
-- defining a record signature, this time I inline the fields into the
-- arguments of the predicate.

pred Concrete (conAuthPurse : NAME -> ConPurse, ether : set MESSAGE, archive : Logbook) {
-- relation is functional
	all n : NAME | lone n.conAuthPurse
-- specification constraints
	all n : NAME | n in conAuthPurse.ConPurse implies n.(conAuthPurse).name = n
	all n : NAME, pd : PayDetails | n -> pd in archive.log implies n in conAuthPurse.ConPurse	
-- coin sharing constraints
	no disj n1, n2 : NAME | some n1.conAuthPurse.balance + n2.conAuthPurse.balance
	no p : ConPurse, pd : PayDetails {
		p in NAME.conAuthPurse
		pd in NAME.(archive.log)
		some p.balance & pd.value
	}

}

-- A Concrete world.

sig ConWorld {
	conAuthPurse : NAME -> ConPurse,
	ether : set MESSAGE,
	archive : Logbook
} {
	Concrete (conAuthPurse, ether, archive)
}

-- Unicity constraint for concrete worlds

fact {
	no disj c1, c2 : ConWorld {
		c1.conAuthPurse = c2.conAuthPurse
		c1.ether = c2.ether
		c1.archive = c2.archive
	}
}