Spacetime Programming
Spacetime programming is a programming language on top of Java to describe search strategy when exploring a state-space, for example in constraint satisfaction problems. Spacetime started as a research project and is formally described in this dissertation. A Java project integrating spacetime code can be set up in 5 minutes with the Maven build system.
Spacetime is based on two main paradigms: synchronous programming and concurrent constraint programming (CCP). These two paradigms are not mainstream and it is very likely that you did not hear about these two paradigms before. In this tutorial, we walk you through the syntax and semantics of spacetime with various examples. Our goal is to keep the tutorial accessible to programmers and computer scientists, and to give you an idea of the kind of problems this language can solve.
Independently of your background, a first step is to read the Getting Started chapter. We introduce the concepts of Synchronous Programming and the syntax of spacetime through several small examples. We make sure the build system is working out for you. Secondly, we introduce some novelties of Spacetime Programming with examples stemming from constraint satisfaction problems such as Sudoku. We next consider the more advanced concept of Universe which is useful to design restarting search strategies. Finally, we go through a full application of this language by designing a interactive search strategy for an application of musical composition.
The code is available on github.
Note that this tutorial is a work-in-progress.
Syntax cheat sheet
p
and q
are statements, e
is an expression, x
a variable identifier and st
is a spacetime attribute (either single_space
, single_time
and world_line
).
Statements | Description |
---|---|
st T x = e | Declares the variable x of type T with the spacetime st . |
when e then p else q end | Executes p if e is equal to true , otherwise q . |
x <- e | Joins the information of e into x . |
o.m(x1,..,xn) | Executes the Java method m on the object o . Variables must be annotated by read , write or readwrite (read by default). |
pause | Delays the execution to the next instant. |
pause up | Delays and gives the control back to the upper universe. |
stop | Delays and gives the control back to the host language. |
par p ||q end | Executes concurrently p and q . Terminates when both terminate. |
par p <> q end | Same as || but terminates in the next instant if one process terminates before the other (weak preemption). |
p ; q | Executes p , when it terminates, executes q . |
loop p end | Executes indefinitely p . When p terminates it is executed from its beginning again. |
space p end | Creates a new branch. All world_line variables are copied and are modified by p when the node is popped. |
prune | Indicates that a branch should be pruned. |
abort when e in p end | Executes p unless e is true , in which case the statement terminates in the current instant. |
suspend when e in p end | Executes p in every instant in which e is false . |
universe with x in p end | Executes p in a universe with the queue x . |