Timed Model Simulation in Maude


ABS models can be augmented with timing information and their execution simulated on the Maude backend. The timed Maude backend adds a model of a clock counting up from 0. This section describes language features related to this clock. Most of these features are implemented on the Maude backend and ignored on the Java backend.

Language Elements


The current value of the clock can be accessed with the now() function, which returns a value of type Time. (now() is implemented using the function currentms(), which returns an integer value and is also available on the Java backend, where it returns the system time.)

Note that now is not a real function, since its value changes over time.

data Time = Time(Rat timeValue);  // this is part of the ABS standard library
Time t = now();

Advancing time in the COG

The duration(min, max) statement causes execution on the current COG to be blocked for at least min and at most max time units. This is used to simulate methods taking some amount of time for execution. (In the Java backend, time passes on its own, so the duration statement does nothing there.)

// Time will advance between 3 and 5 units during execution of m
Unit m() {
  duration(3, 5);

Advancing time in a process

The statement await duration(min, max) causes the running process to be suspended for at least min time units. The difference to the duration statement is that other processes in the same COG are allowed to run while the process is suspended. Similar to the duration statement, this is for simulation purposes, so await duration statements do not suspend the process in the Java backend.

// Method m will return after at least 3 time units
Unit m() {
  await duration(3, 5);

Expressing deadlines

The deadline (remaining time to execute) for a process can be accessed via the deadline() function, which returns a value of type Duration. Deadlines are relevant for timed Maude simulations; a process can detect whether it missed its deadline by inspecting the return value of deadline().

Note that deadline is not a real function, since its value changes over time.

// This datatype is part of the ABS standard library
data Duration = Duration(Rat durationValue) | InfDuration;

Duration time_to_complete = deadline(); // can be infinite
if (deadline() == Duration(0)) {
  // We missed the deadline ...

Deadlines are set at process creation time, i.e. at the calling site. Synchronous and asynchronous method calls can be decorated with [Deadline: e] annotations; the default deadline is InfDuration.

// Give m 17 time units to execute
[Deadline: Duration(17)] o!m();

// Do not give a deadline; this is the default behavior
[Deadline: InfDeadline] o.n();

On the Java backend, at the moment deadline annotations are ignored and deadline() always returns InfDuration.