Money settlement between businesses always follows a **process**

## Examples of business processes

### Process 1

- A is required to send 10 trucks of goods to B between times T0 and T1
- When a truck arrives, it is checked and receipt is signed by responsible from A and responsible from B
- After T1, if all the trucks have arrived, A sends an invoice to B
- B pays within 30 days

### Process 2

- A is required to send 10 trucks of goods to B between times T0 and T1
- After T1, only 9 trucks have arrived
- A requests B for an agreement "we will deliver the last truck in the next 3 business days"
- B refuses the agreement
- A sends an invoice for 9 trucks minus contractual penalty
- B pays within 30 days

### Process 3

- A is required to send 10 trucks of goods to B between times T0 and T1
- After T1, only 9 trucks have arrived
- A requests B for an agreement "we will deliver the last truck in the next 3 business days"
- B accepts the agreement : T1 is moved to T1 + 3, the contractual penalty is doubled
- (the last truck doesn't arrive)
- A sends an invoice for 9 trucks minus contractual penalty
- B pays within 30 days

### Process 4

- A buys a house from B
- C agrees to lend money to A
- C sends the money to B
- B adds a hypothec on the house and transfers the house to A
- A has to make monthly payments to C
- Once payments are finished, hypothec on the house is removed

### Process 5

- A buys house from B, the house has a hypothec and monthly payments to C
- X buys the hypothecated house from A, now X needs to make the payments to C
- if X fails to make the monthly payment to C, the house is sent back to C

### Process 6

- A owns a house
- A borrows money from B using 50% of his house as collateral
- A borrows money from C using 50% of his house as collateral
- A fails a monthly payment to B
- B now fully owns 50% of the house
- X buys the 50% hypothec from A and 50% ownership from B
- X continues the payments to C
- After all the payments are over, X owns the house

## Concepts

Processes are less about making sure that the money is paid and more about managing the complexity of thousands of simultaneous business agreements.

Imagine a company specialized in transportation, or lending for the housing market. They have thousands of customers in different stages of each process and they need to have global visibility of their position.

The important concepts are
- **FT** : anything that behaves like money
- **NFT** : rights (e.g. a "talk stick" is a stick that allows you to talk in a meeting. You cannot talk without the stick. You need to request it from the person that has it if you want to talk. There may be a timer on how long you can keep the stick. The talk stick materializes "the right to talk")
- **Time**
- External **messages**

We need to design a process language that
- is obvious for most professionals
- covers our typical use cases

There are some external business process modeling (BPM) languages but they seem a little convoluted (https://en.wikipedia.org/wiki/Business_process_modeling)


But the global idea is correct
- A process is a sequence of states S1 -> S2 -> S3 -> S4
- Each state is guarded by a logical expression over variables
- The state transitions can modify those variables
- External messages (signed messages) request a change of state

### Process 1 seen as a state machine

S
condition: double signature of agreement
state: N = 0

S -> C(0)
pre-condition: message at T > T0 signed by A
state: N = 0

C(N) -> C(N+1)
pre: message signed by A and B (asserting a truck has arrived)
state: N integer

C(N) -> I
pre: message signed by A at time T > T1 (requesting to move to invoice) && N = 10
state: N integer

### Parametric transition systems

Automata + variables and guarded transitions is almost the core language of parametric model-checking systems (Cubicle in OCaml allows more complex code to be present in the transitions). DOFP is in favor of using a sublanguage of parametric transition systems

init (unit)

init (unit) -> count (int)
| when m == signed(A,B, (Init, t)) && T > T0  // Syntax to deconstruct messages

count (int) -> count (int)
| {N} when m == signed(A,B, (Truck, t)) && t < T1 -> { N : N  + 1 }

count (int) -> invoice (unit)
| {N = 10} when m == signed(A, (Invoice, t)) && t > T1 -> {}

These systems can easily be transformed into a diagram for visual aid

digraph {
init -> "count n " [fontname="Courier" label="  T > 0"]
"count n " -> "count n " [fontname="Courier" label="  n -> n+1"]
"count n " -> invoice [fontname="Courier" label="  n == 10 && T > 10"]
}

Such a process language can represent most of the current processes when augmented with
- the ability to recognize messages and signatures
- simple primitives (*transfer*, etc)

The only problem is the **representation of property**, which is exemplified by processes 4,5,6 above, in other words
- how to limite the usage of a resource (a hypothecated house)
- how to sell a complex resource (a hypothecated house)

### More complex rewriting system

Fred suggests more complex processes can be written as a rewriting system over a store of objects

resource S
resource Truck
resource C(int)

start: () -> S * C(0)

send_truck: S -> S * Truck 

count_truck: Truck * C(i) -> C(i + 1)

pay: C(10) -> ()
condition: T <= T1

A production rule like ``S -> S * Truck`` requires a ``S`` object in the store, that it will consume at each usage, and generate in exchange an ``S`` and a ``Truck``. This is reminiscent of the [RETE algorithm](https://en.wikipedia.org/wiki/Rete_algorithm).

If there are rules of the type ``C(i) -> C(j) * C(k)`` the number of states can be infinite even if parametrized. In the absence of such rules, the system is equivalent to a state (s,t,c) and the transitions

transitions
| -> (0,0,0)
| (0,0,0) -> (1,0,1)
| (1,t,_) -> (1,t+1,_)
| (_,t,c) when t >= 0 -> (1,t-1,c+1) 
| (_,_,10) -> .

where ``(_,_,k) ~ C(k)``

## Blockchain representation of property and rights

Currently blockchain has 2 concepts
- **full property** : you own an address and you can do whatever you want with it
- **holdings** : a group of people agree to create a holding, the rules / rights of the holding participants are described in a smart contract, and the holding has full property of the assets

Holding rules / rights are **opaque** and are not **future proof** : if you don't plan in advance all the uses cases (for instance the capability of selling your "place" in the holding) then that freedom is removed forever and unrecoverable.

Because **holding rules are positive** (you are forbidden to do anything except what is allowed in the rules), holding contracts are lengthy for very little usefulness. **Real life contracts are negative** (you are allowed to do anything you want except what is limited by the contract).

## Internal representation