PSF - Process Specification Formalism

A small Factory with input and output queue

Description

Specification

data module S-Products
begin
    exports
    begin
	functions
	    eq-prod : PRODUCT # PRODUCT -> BOOLEAN
	    error : -> PRODUCT
    end
    imports
	Products, Booleans
end S-Products

process module S-Factory
begin
    imports
	Factory,
	Sequences {
	    Elements bound by [
		ITEM -> PRODUCT,
		eq -> eq-prod,
		error-element -> error
	    ] to S-Products
	}
    atoms
	q-input : PRODUCT
	q-output : PRODUCT
	q-send-input : PRODUCT
	q-read-output : PRODUCT
	comm-q-input : PRODUCT
	comm-q-output : PRODUCT
    processes
	Start-Q-Factory
	In-Queue : SEQ
	Out-Queue : SEQ
    sets
	of atoms
	    Q-H = { input(p), output(p), q-send-input(p), q-read-output(p)
		    | p in PRODUCT }
    communications
	q-send-input(p) | input(p) = comm-q-input(p) for p in PRODUCT
	q-read-output(p) | output(p) = comm-q-output(p) for p in PRODUCT
    variables
	q : -> SEQ
    definitions
	Start-Q-Factory = encaps(Q-H,
	    In-Queue(empty-sequence) || Start || Out-Queue(empty-sequence))
	In-Queue(q) = sum(p in PRODUCT-set,
		    q-input(p) . In-Queue(q ^ p) )
	    +   [not(eq(q, empty-sequence))=true] ->
		    q-send-input(first(q)) . In-Queue(tail(q))
	Out-Queue(q) = sum(p in PRODUCT-set,
		    q-read-output(p) . Out-Queue(q ^ p) )
	    +   [not(eq(q, empty-sequence))=true] ->
		    q-output(first(q)) . Out-Queue(tail(q))
end S-Factory

Compilation

Assuming the specification resides in file S-Factory, it should be compiled with the command:
% psf -s S-Factory.til

Simulation

Compilation gives the file S-Factory.til, which can be simulated with the command:
% sim S-Factory.til
Choose Start-Q-Factory 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 qin-out rect 22 30 7 15 ""
Anim::CreateQueue qin [expr [Anim::Dim qin-out e,x] + 1] 30 10 1 -anchor w
Anim::CreateItem qin-in rect [expr [Anim::DimQ qin e,x] + 7] 30 7 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 qout-in rect [Anim::Dim s6 x] 107 12 8 ""
Anim::CreateQueue qout [Anim::Dim qout-in x] [Anim::Dim qout-in n,y] 1 5 \
    -orient vertical -anchor s
Anim::CreateItem qout-out rect [Anim::DimQ qout x] \
    [expr [Anim::DimQ qout n,y] - 9] 12 8 "Out"

Anim::CreateLine ins1 pos [Anim::Dim s1 x] [Anim::DimQ qin s,y] item s1 n \
    -arrow last
Anim::TextposLine ins1 ins1 e
Anim::CreateLine outs6 item s6 n pos [Anim::Dim qout-in x] \
    [Anim::Dim qout-in s,y] -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

Anim::CreateBox info queues -side top -ipadx 1 -ipady 1 -expand -bw 2 -relief groove
Anim::CreateBox queues queueinput -side left
Anim::CreateLabel queueinput inputtext "queue In" -width 9 -anchor w
Anim::CreateLabel queueinput inputvar q-input -var -bw 1 -relief sunken -width 2
Anim::CreateBox queues queueoutput -side left
Anim::CreateLabel queueoutput outputtext "queue Out" -width 9 -anchor w
Anim::CreateLabel queueoutput outputvar q-output -var -bw 1 -relief sunken -width 2

Anim::InitVar q-input 0
Anim::InitVar q-output 0

Anim::CreateBox info table -side top -bw 2 -relief groove
Anim::CreateBox table header -side left
Anim::CreateLabel header col0 "" -width 6
Anim::CreateLabel header col1 "A" -width 2
Anim::CreateLabel header col2 "B" -width 2
Anim::CreateBox table row1 -side left
Anim::CreateLabel row1 input input -width 6 -anchor w -bw 1
Anim::CreateLabel row1 inpA input(A) -var -width 2 -bw 1 -relief sunken
Anim::CreateLabel row1 inpB input(B) -var -width 2 -bw 1 -relief sunken
Anim::CreateBox table row2 -side left
Anim::CreateLabel row2 output output -width 6 -anchor w -bw 1
Anim::CreateLabel row2 outpA output(A) -var -width 2 -bw 1 -relief sunken
Anim::CreateLabel row2 outpB output(B) -var -width 2 -bw 1 -relief sunken

Anim::InitArray input [list A 0 B 0]
Anim::InitArray output [list A 0 B 0]

proc ANIM_action {atom} {
    global q-input q-output input output
    if {[regexp {^q-input\((.*)\)$} $atom match arg1]} {
	Anim::AddQueue qin $arg1
	incr q-input
	incr input($arg1)
    } elseif {[regexp {^comm-q-input\((.*)\)$} $atom match arg1]} {
	Anim::SubQueue qin
	incr q-input -1
	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 {^comm-q-output\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText outs6
	Anim::DeactivateLine outs6
	Anim::AddQueue qout $arg1
	incr q-output
    } elseif {[regexp {^q-output\((.*)\)$} $atom match arg1]} {
	Anim::SubQueue qout
	incr q-output -1
	incr output($arg1)
    }
}

proc ANIM_choose {atom} {
    if {[regexp {^q-input\((.*)\)$} $atom match arg1]} {
	Anim::AddList qin-in $match
    } elseif {[regexp {^comm-q-input\((.*)\)$} $atom match arg1]} {
	Anim::AddList qin-out $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 {^comm-q-output\((.*)\)$} $atom match arg1]} {
	Anim::AddList qout-in $match
    } elseif {[regexp {^q-output\((.*)\)$} $atom match arg1]} {
	Anim::AddList qout-out $match
    }
}
Assuming the animation resides in file s-factory.tcl we can start the animation with the command:
% simanim S-Factory.til s-factory.tcl