A small Factory

• Description
• Specification
• Compilation
• Simulation
• Animation

Description

The factory consist of an input and output, some stations and conveyer belts. It produces the products A and B, which take slightly different routes through the factory.

Specification

data module Products
begin
    exports
    begin
	sorts
	    PRODUCT
	functions
	    A : -> PRODUCT
	    B : -> PRODUCT
    end
end Products

data module Stations
begin
    exports
    begin
	sorts
	    STATION
	functions
	    1 : -> STATION
	    2 : -> STATION
	    3 : -> STATION
	    4 : -> STATION
	    5 : -> STATION
	    6 : -> STATION
	    eq-stat : STATION # STATION -> BOOLEAN
	    next : STATION # PRODUCT -> STATION
    end
    imports
	Booleans, Products
    variables
	x : -> STATION
	y : -> STATION
	p : -> PRODUCT
    equations
    [1] eq-stat(x, x) = true
    [2] not(eq-stat(x, y)) = true
    [3] next(1, p) = 2
    [4] next(2, p) = 3
    [5] next(3, A) = 4
    [6] next(3, B) = 5
    [7] next(4, p) = 5
    [8] next(5, p) = 6
end Stations

process module Factory
begin
    imports
	Stations
    atoms
	input : PRODUCT
	output : PRODUCT
	read-input : PRODUCT
	send-input : PRODUCT
	comm-input : PRODUCT
	read-output : PRODUCT
	send-output : PRODUCT
	comm-output : PRODUCT
	to-belt : STATION # STATION # PRODUCT
	from-belt : STATION # PRODUCT
	comm-belt : STATION # STATION # PRODUCT
    processes
	Start
	Input
	Stations
	Station : STATION
	Output
    sets
	of PRODUCT
	    PRODUCT-set = { A, B }
	of STATION
	    STATION-set = { 1, 2, 3, 4, 5, 6 }
	of atoms
	    H = { send-input(p), read-input(p), send-output(p), read-output(p),
		    to-belt(x, y, p), from-belt(y, p)  | p in PRODUCT,
		    x in STATION, y in STATION }
    communications
	send-input(p) | read-input(p) = comm-input(p)
	    for p in PRODUCT
	send-output(p) | read-output(p) = comm-output(p)
	    for p in PRODUCT
	to-belt(s1, s2, p) | from-belt(s2, p) = comm-belt(s1, s2, p)
	    for s1 in STATION, s2 in STATION, p in PRODUCT
    variables
	s : -> STATION
    definitions
	Start = encaps(H, Input || Stations || Output)
	Input = sum(p in PRODUCT-set, input(p) . send-input(p)) . Input
	Stations = merge(s in STATION-set, Station(s))
	Station(s) =
		[eq-stat(s, 1) = true] -> (
		    sum(p in PRODUCT,
			read-input(p) . to-belt(s, next(s, p), p)
		    ) . Station(s)
		)
	    +   [eq-stat(s, 6) = true] -> (
		    sum(p in PRODUCT,
			from-belt(s, p) . send-output(p)
		    ) . Station(s)
		)
	    +   [and(not(eq-stat(s, 1)), not(eq-stat(s, 6))) = true] -> (
		    sum(p in PRODUCT,
			from-belt(s, p) . to-belt(s, next(s, p), p)
		    ) . Station(s)
		)
	Output = sum(p in PRODUCT, read-output(p) . output(p)) . Output
end Factory

Compilation

We make use of the library of PSF, so we have to set an environment variable in order to let the compiler find the library.

% setenv PSFPATH .:<psf-install-dir>/lib/psflib

This works for csh and the like, for other shells see the documentation of these shells.

Assuming the specification resides in the file Factory compilation can be done with the command:

% psf Factory

Simulation

Compilation gives the file Factory.til, which can be simulated with the command:

% sim Factory.til

Choose Start as start process.

Animation

With the tool simanim we can combine the simulation with animation. For the animation we use:

Anim::Windows 340 200 -text 30 10

Anim::CreateItem inp rect 30 30 15 15 "In"
Anim::CreateItem s1 rect 30 100 15 15 "1"
Anim::CreateItem s2 rect 100 100 15 15 "2"
Anim::CreateItem s3 rect 170 100 15 15 "3"
Anim::CreateItem s4 rect 240 100 15 15 "4"
Anim::CreateItem s5 rect 240 170 15 15 "5"
Anim::CreateItem s6 rect 310 170 15 15 "6"
Anim::CreateItem out rect 310 100 15 15 "Out"

Anim::CreateLine ins1 item inp s item s1 n -arrow last
Anim::TextposLine ins1 ins1 e
Anim::CreateLine outs6 item s6 n item out s -arrow last
Anim::TextposLine outs6 outs6 w

Anim::CreateLine s1s2 item s1 e item s2 w -width 15
Anim::CreateLine s2s3 item s2 e item s3 w -width 15
Anim::CreateLine s3s4 item s3 e item s4 w -width 15
Anim::CreateLine s3s5 item s3 s pos [Anim::Dim s3 x] [Anim::Dim s5 y] \
    item s5 w -width 15
Anim::CreateLine s4s5 item s4 s item s5 n -width 15
Anim::CreateLine s5s6 item s5 e item s6 w -width 15

proc ANIM_action {atom} {
    if {[regexp {^input\((.*)\)$} $atom match arg1]} {
	Anim::CreateText ins1 "$arg1"
	Anim::ActivateLine ins1
    } elseif {[regexp {^comm-input\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText ins1
	Anim::DeactivateLine ins1
	Anim::CreateItem AT1 rect [Anim::Dim s1 x] [Anim::Dim s1 y] \
	7 7 "$arg1" -free -color 1
    } elseif {[regexp {^comm-belt\(3, 4, .*\)$} $atom match arg1]} {
	Anim::Move AT3 rightto [Anim::Dim s4 x] -newid AT4
    } elseif {[regexp {^comm-belt\(3, 5, .*\)$} $atom match arg1]} {
	Anim::Move AT3 downto [Anim::Dim s5 y] rightto [Anim::Dim s5 x] -newid AT5
    } elseif {[regexp {^comm-belt\(4, 5, .*\)$} $atom match arg1]} {
	Anim::Move AT4 downto [Anim::Dim s5 y] -newid AT5
    } elseif {[regexp {^comm-belt\((.*), (.*), .*\)$} $atom match arg1 arg2]} {
	Anim::Move AT$arg1 rightto [Anim::Dim s$arg2 x] -newid AT$arg2
    } elseif {[regexp {^comm-output\((.*)\)$} $atom match arg1]} {
	Anim::DestroyItem AT6
	Anim::CreateText outs6 "$arg1"
	Anim::ActivateLine outs6
    } elseif {[regexp {^output\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText outs6
	Anim::DeactivateLine outs6
    }
}

proc ANIM_choose {atom} {
    if {[regexp {^input\((.*)\)$} $atom match arg1]} {
	Anim::AddList inp $match
    } elseif {[regexp {^comm-input\((.*)\)$} $atom match arg1]} {
	Anim::AddList s1 $match
    } elseif {[regexp {^comm-belt\((.*), (.*), .*\)$} $atom match arg1 arg2]} {
	Anim::AddList AT$arg1 $match
    } elseif {[regexp {^comm-output\((.*)\)$} $atom match arg1]} {
	Anim::AddList s6 $match
    } elseif {[regexp {^output\((.*)\)$} $atom match arg1]} {
	Anim::AddList out $match
    }
}

Assuming the animation resides in file factory.tcl we can start the animation with the command:

% simanim Factory.til factory.tcl