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 readablity 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 and storage cells needed. The set of names in scope at any time are those of all currently loaded scripts, together with the names of the standard environment (this is the asmgofer prelude), which are always inscope. 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

`: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 scripts 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`	set command line options
`:set`	help on command line options
`:names [pat]`	list names currently in scope
`:info`	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

Comands 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 any type is a legal AsmTerm. Therfore the user sometimes has to specify that terms of a particular types 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, ornage 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 inconsitent update. Note that you can use the value asmDefault to delete something, e.g.

  ? fire (do trafficLights(N):= asmDefault)

  ()

  ? assocs trafficLights

  [(East,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, Joachim Schmid