An Overview of AsmGofer

Wolfram Schulte and Joachim Schmid

AsmGofer is an advanced Abstract State Machine (ASM) programming system, which runs under several platforms (Unix-based or MS-based operating systems). The aim of the AsmGofer system is to provide a modern ASM interpreter embedded in the well known functional programming language Gofer. Gofer is a subset of Haskell -- the de-facto standard for strongly typed lazy functional programming languages. The purpose of this short introduction is to give a brief overview of the main features of AsmGofer and to describe its use:

Instead of an introduction: An example

An AsmGofer program (better called "script") is a collection of signatures, rules, functions and data structures which we are interested in computing. The order in which these entities are given is not significant. Here is a very simple example of an AsmGofer script for a depth first traversal of a directed graph. For simplicity we assume that the nodes of the graph are labelled with integers. The edges are given with a successor function.

type Node = Int
succs :: Node -> {Node}

The range of the successor function is defined using the data structure set, i.e. {Node}. A set is a special version of the commonly used data structure list. An example graph might be a graph that connects 1 to 2 and 3 (i.e. the successors are described by the set {2,3}), 2 to 3 and 4, 3 to 2, 4 to 5, 6 to 1 and for any other node there are no successors.

succs 1 = {2,3}
succs 2 = {3,4}
succs 3 = {2}
succs 4 = {5}
succs 6 = {1}
succs _ = {}

When traversing the graph, we have to remember the visited nodes. We store them in a dynamic function, which is initially nowhere defined (i.e. described by the empty association list).

visited :: Dynamic (Node -> Bool)
visited = initAssocs "visited" []

Remark: the name "visited" is only used for error reporting. This will be eliminated in the future.

For example, let us compute all reachable nodes starting from the node with number 1. We introduce a dynamic variable called todo, that holds all nodes that are still to be processed.

todo :: Dynamic [Node]
todo = initVal "todo" [1]

The traversal of the graph is performed by the following rule called traverse (++ is list concatenation, head and tail select the head and tail of the list.)

traverse :: Rule()
traverse = if todo == [] then
             skip
            else
             if not(visited(head todo)) then do
               visited(head todo) := True
               todo := expr2list(succs(head todo)) ++ tail todo
              else
               todo := tail todo

Notice the absence of syntactic sugar - AsmGofer is, by design, rather terse. There are no mandatory signatures, although the language is strongly typed. For reasons of readability we nevertheless gave signatures such as

succs:: Node -> {Node}

There are no semicolons at the end of definitions - the parsing algorithm makes intelligent use of layout. Function application is just denoted by juxtaposition, instead of writing f(x) we wrote f x.

The AsmGofer Environment

The AsmGofer system is interactive. It is invoked from a shell by the command

asmgofer [file]

where ‘file’ (an optional parameter) is the pathname of a file containing an AsmGofer script. We assume that we have stored the previous definitions in a file called "traverse.gs" and that we have called asmgofer with the latter. After parsing and context checking the prompt

occurs, indicating that you are talking to the AsmGofer command interpreter. This activity is called a “session”. The basic action is to evaluate expressions, supplied by the user at the terminal, in the environment established by the current script. For example evaluating the dynamic function todo in the context of the given script produces

? todo [1]
(6 reductions, 29 cells)

The first line shows the result, the last line shows the number of reductions and storage cells needed. The set of names in scope at any time is those of all currently loaded scripts, together with the names of the standard environment (this is the asmgofer prelude), which are always in scope. For instance, we can also evaluate

? todo ++ todo [1,1]
(13 reductions, 42 cells)

Remark: Alternatively we could have written $$ ++ $$ since $$ always denotes the value of the last evaluation. If we want to fire the traverse rule once, we evaluate

? fire1(traverse)
() (42 reductions, 99 cells, 1 steps)

which means that the ASM described by the loaded script has made one (non-visible) step -- the result is the empty tuple. Notice that you have to evaluate rules. You can not fire rules by themselves. You can inspect the extension of the visited state as an association list by entering

? assocs(visited)
[(1,True)] (7 reductions, 28 cells)

If we want to run the ASM until a fixpoint occurs, you enter:

? fixpoint(traverse)
(208 reductions, 448 cells, 6 steps)

For more functions, see the appendix.

Any command not beginning with : is assumed to be an expression to be evaluated. The following commands are available during a session

Command	Description
`:load <filename>`	load scripts from specified files, clear all files except prelude
`:load`	load last specified files, clear all files except prelude
`:also <filename>`	load additional script files
`:reload`	repeat last load command
`:project <filename>`	use project file <filename>
`:project`	use last project
`:edit <filename>`	edit file
`:edit`	edit last file
`:type <expr>`	print type of expression
`:?`	display this list of commands
`:set <options>`	set command line options
`:set`	help on command line options
`:names [pat]`	list names currently in scope
`:info <names>`	describe named objects (the *pattern matches any string)
`:find <name>`	edit file containing definition of name
`:!command`	command shell escape
`:cd dir`	change directory
`:gc`	force garbage collection
`:quit`	exit AsmGofer interpreter

Commands may be abbreviated to :c where c is the first character of the full command. The AsmGofer compiler works in conjunction with an editor and scripts are automatically recompiled after edits, and any syntax or type errors signaled immediately. The polymorphic type system permits a high proportion of logical errors to be detected at compile time. The location of the prelude must be specified in the variable GOFER. The editor can be specified in the variable EDITLINE. In my installation these variables are specified as follows:

export GOFER=/usr/AsmGofer2/Preludes/prelude-asm
export EDITLINE=vi +%d %s

The AsmGofer Language Extensions

AsmGofer is a conservative extension of Gofer. Although we had to change the run time system (to introduce updatable functions) no changes to the type system were made. New syntactic constructs are

<expr> ::= ...
        |   forall <quals> do <exp>
        |   choose <quals> do <exp>
        |   create <var>,...,<var> <expr>
        |   <exp> := <exp>
        |   skip

The types are

skip :: Rule ()
(:=) :: AsmTerm a => a -> a -> Rule ()
forall <quals> do <exp> :: Rule ()
choose <quals> do <exp> :: Rule ()
create <var>,...,<var> <expr> :: Rule ()

The Rule type is builtin. It guarantees parallel evaluation. The effect of a rule is only visible if rules are fired! Suppose we want to reset the state in our previous example. Then we could write:

? fire1 (do todo := {1}
            forall x <-: dom(visited) do
               visited(x) := False
        )

Note that the already existing "do" works as block...endblock. The primitive choose among is not supported in the current release. There is already an experimental version of it available, but it is not yet stable.

A final note

ASMs only allow variables and first order functions to be dynamic. However, since Gofer supports higher order functions, not every type is a legal AsmTerm. Therefore the user sometimes has to specify that terms of a particular type can be used in the ASM extension, i.e. the user must specify the type as an AsmTerm type. For an example see below. Furthermore, to check whether updates are consistent, we have to check them for equality and for reasons of efficiency we also require an ordering on the domain. However, since Gofer supports higher order functions, there is no builtin equality (and order). As a consequence, as soon as you use more complex types than the basic types Int, Float, Char or String you must give instances for the class Eq (and AsmOrd). If you do not give an instance for Eq (and AsmOrd) structural equality is the default.

Suppose you want to model a crossing having 4 traffic lights each one can show the colours red, orange and green, and you want them initially in the state orange then you could write -- Asm(Gofer) Declarations

data Where = N | E | W | S
data Colour = Red
            | Orange
            | Green
trafficLights :: Where -> Colour
trafficLights = initAssocs "trafficLights" [(x,Orange) | x <- [N,E,W,S]]

instance AsmTerm Where
instance AsmTerm Colour

Now you can write:

? fire1 (do trafficLights(N) := Red
            trafficLights(N) := Orange)
ERROR: inconsistent update
*** dynamic function : "trafficLights"
*** expression (new) : Orange
*** expression (old) : Red

which is -- as expected -- an inconsistent update. Note that you can use the value asmDefault to delete something, e.g.

? fire1 (do trafficLights(N) := asmDefault)
()
? assocs trafficLights
[(E,Orange),(W,Orange),(S,Orange)]

Alternatively you can say that a normal value should play the role of asmDefault, i.e. instead of specifying that any trafficLight is Orange you say that Orange is the default. If you change the running example to

trafficLights :: Where -> Colour
trafficLights = initAssocs "trafficLights" []

(Asm)Gofer Declarations:

instance AsmTerm Where
instance AsmTerm Colour where
  asmDefault = Orange

you can evaluate

? trafficLights(N)
Orange

The AsmGofer Prelude

The prelude contains the signatures and definitions of all functions available in AsmGofer. For details see the prelude directory in the distribution.

Last modified on June 4, 2001