Example CSP programs

Smoker’s Problem

Three chain smokers are together in a room with a vendor of cigarette supplies. To make and use a cigarette, each smoker needs three ingredients: tobacco, paper, and matches, all of which the vendor has ample supply. One smoker has his own tobacco, a second has his own paper, and the third has her own matches. The action begins when the vendor puts two of the ingredients on a table. When the appropriate smoker is done, he or she wakes up the vendor, who the puts down two more ingredients (randomly), unblocking another smoker.

HaveT::*[Paper?p AND Matches?m -> smoke; Vendor!done]
HaveM::*[Paper?p AND Tobacco?t -> smoke; Vendor!done]
HaveP::*[Tobacco?t AND Matches?m -> smoke; Vendor!done]
Paper::*[vendor?start -> [HaveT!p -> HaveT?done;
[] HaveM!p -> HaveM?done]
Matches::*[ vendor?start ->[HaveT!m -> HaveT?done;
[] HaveP!m -> HaveP?done]
Tobacco::*[ vendor?start ->[HaveM!t -> HaveM?done;
[] HaveP!t -> HaveP?done]
[Paper!start -> null
[] Matches!start -> null
[] Tobacco!start-> null]

[Paper!start -> null
[] Matches!start -> null
[] Tobacco!start-> null]

[HaveT?done -> null
[] HaveM?done -> null
[] HaveP?done -> null]
notes: The vendor randomly chooses to start one of the resources (paper, tobacco or matches). It then does the same thing to start another resource. It waits until one of the smokers signals completion before starting the process again.


Networked Philosophers

 Consider a system with a large number of nodes interconnected by an arbitrary connected graph. Each node is connected to one or more (usually several) other nodes. Each pair of connected nodes shares a unique resource. At random times a node needs to perform a function that requires exclusive access to all of the resources it shares with all of its neighbors. Each node has a list of the resources is needs to perform the function.


Assign each resource a unique number. Assume that each node has a list, called needs, of the resources it needs, sorted in numerical order. When a node wants to perform a function requiring the resources, it acquires the resources in numerical order. Acquiring the resources in order prevents deadlock.

 Node[1..N]::*[int needs(1..K); int i, K;
    i = 1;
    *[i < K AND resource[needs(i)]!lock -> i = i + 1]
    [resource[needs(K)]?lock —> perform function]
    i = 1;
    *[i <= K AND resource[needs(i)]!unlock -> i = i + 1]

resource[1..M]::*[ Node[r]?lock -> Node[r]?unlock
                        []Node[s]?lock -> Node[s]?unlock

 notes: The resource process waits for a lock request from either node that shares it. Once a node locks a resource, another node cannot access the resource until the first node executes the unlock rendezvous. The nodes lock all of the necessary resources in order. Upon locking the last resource, it can perform the function.



Four people are sharing the use of tools - a hammer and 2 mallets - to manufacture small components. Each object is made by driving a peg into a block. A pair, consisting of a peg and a block, is referred to as a job. The jobs arrive sequentially on a conveyer belt and completed jobs depart on a conveyer belt. The jobshop could involve any number of workers called jobbers, sharing more or fewer tools. The jobs that arrive at the conveyer have varying degrees of difficulty: easy, moderate, hard. An easy job requires no tool (manual), a moderate job can use either a hammer or mallet, but a hard job requires a hammer. Jobbers may therefore non-deterministically compete for the use of the hammer and mallet, as well as who takes the next job.


inbelt::*[jobber[1..4]!easy -> null
            [] jobber[1..4]!moderate -> null
            []jobber[1..4]!hard -> null]

outbelt::*[jobber[1..4]?done -> remove completed job]

hammer::*[jobber[1..4]!get -> jobber[1..4]?return]

mallet[1..2]::*[jobber[1..4]!get -> jobber[1..4]?return]

jobber[1..4]::*[inbelt?easy -> assemble; outbelt!done
			[]inbelt?moderate-> [hammer?get -> assemble; hammer!return; outbelt!done;
							[] mallet[1..2]?get -> assemble; mallet[1..2]!return; outbelt!done]
[			]inbelt?hard -> [hammer?get -> assemble; hammer!return; outbelt!done]



notes: The inbelt process creates jobs of different difficulty and sends them to any waiting jobber. Once the jobber acquires a job, it acquires the necessary tools. Note that there is no effort to reserve the hammer for hard jobs. It might be randomly selected for a medium job from the tools available. Once the job is assembled, the tools are returned and the job passed to the outbelt.