--------------------------------------------------------------
--
--      sample.csp  
--
--      sueo@ecs.syr.edu,  8 Sept 1999
--
--
--------------------------------------------------------------

-- Throughout this file, TPC refers to the class textbook: 
-- Bill Roscoe's __Theory and Practice of Concurrency__.

-- This file is intended to display some of the basic features
-- of machine-readable CSP.  Much more extensive examples can 
-- be found in the FDR2 manual or in the sample scripts included
-- in the FDR/ProBE distributions; on our system, they're located
-- in the directory  /usr/local/probe/book/examples/

-- First off, end-of-line comments are indicated by "--", such as at 
-- the beginning of these lines.  You can also use block comments 
-- (which can be safely nested) as follows:

{-
   This is a block comment comprising multiple lines.  The manual 
   recommends that the beginning "{-" and end "-}" appear on their 
   own lines, because it's possible to get them confused with sets 
   with a leading unary minus sign.
-}

-------------------------------------------------------------------------
-------------------------------------------------------------------------

-- To start off, it's important to define the events of concern.  
-- Note that we use the keyword "channel", even if we're just talking 
-- about simple events.  

channel east, west, north, south

-- Now, we can define the process for the map we saw in Exercise 1.1.4 
-- of TPC.

-- Note that [] is used to represent external choice.

A = east -> B

B = west -> A [] east -> C [] south -> D

C = west -> B

D = east -> E

E = north -> C [] south -> G

F = north -> D

G = west -> F


-- Now we have some sample specifications, written in process form.

-- The following specification states that the only possible traces 
-- are prefixes of (east west)^n, for all possible n.

EWSpec =  east -> west -> EWSpec

-- The following line asserts that A refines Spec1 (ie, that 
-- every trace of A is also a trace of Spec1).  We can use FDR to 
-- verify (or refute, in this case) this assertion.

assert EWSpec [T= A

-- The following line asserts that every trace of Spec1 is also a trace 
-- of A.  FDR should be able to verify this assertion.

assert A [T= EWSpec

-------------------------------------------------------------------------
-------------------------------------------------------------------------

-- Let's also define some "real" channels, which have various types.
-- Section A.3 of Appendix A of the FDR2 manual discusses the various 
-- options available.  

-- left and right can carry base-4 digits

channel left, right : {0..3}  

COPY = left?x -> right!x -> COPY


-- Here are the examples from HW #1  (Exercise 1.1.8 from TPC)

-- 1.1.8(a)  

FCOPY = left?x -> (right!x -> FCOPY [] left?y -> STOP)

-- 1.1.8(b)

DELAY = left?x -> DELAY1(x)
DELAY1(x) = left?y -> right!x -> DELAY1(y)

-- 1.1.8(d)

LEAKY = left?x -> right!x -> left?x -> right!x -> left?x -> LEAKY

-- an alternative approach, using the conditional

ALT_LEAKY = ALEAK(1)
ALEAK(n) = left?x -> (if n==0 then ALEAK(1) 
                             else right!x -> ALEAK ((n+1) % 3))


channel a, b

X = a-> STOP [] b-> STOP

Y = a ->STOP |~| b -> STOP

-------------------------------------------------------------------------
-------------------------------------------------------------------------

-- traffic_light can carry a value of the user-defined type Color

datatype Color = Red | Yellow | Green

channel traffic_light : Color
channel stop, go

MV_LAW = go -> 
         traffic_light?c -> 
         (if c==Red then stop -> traffic_light.Green -> MV_LAW 
                    else MV_LAW)

OLD_HEAP = go -> 
	   traffic_light?c -> 
	   (if c==Red then stop -> STOP else OLD_HEAP)

SPORTS_CAR = go -> traffic_light?c -> SPORTS_CAR



-------------------------------------------------------------------------
-------------------------------------------------------------------------