Creating and using automata

We're now going to see how automata are created and used. While we will focus here on how to do that in Cell, as opposed to doing it from the host language in mixed-language applications, all the commands we're going to describe have close equivalents in the interface of the generated code.

Automata of either type can only be created inside procedures and not functions. A procedure can declare any number of automaton variables, but it cannot create automata dinamically: all automaton variables are instantiated when a procedure is called, and automatically destroyed when it returns. Automaton instances are also only visible inside the procedure they're declared in and they cannot be passed to other procedures.

Relational automata

In order to see how to manipulate relational automata, we'll write a tiny command line tool that is actually useful in practice. Our application will create a relational automaton, read an initial state for it from a file and a list of messages from another, send each message to the automaton instance in the given order, and save its final state in another file. We'll make use of the Counter automaton we saw in the previous chapters, but the code can be made to work with any automaton type with only trivial changes.

Int Main(String* args) {
  instance : Counter;

  // Checking the argument list
  if |args| != 3:
    Print("Invalid arguments\n");
    return 1;
  ;
  init_state_fname, msg_list_fname, final_state_fname = args;

  // Reading and checking the initial state
  res = ReadValueFromFile(init_state_fname);
  return 1 if res == nothing;
  init_state = value(res);
  if not init_state :: Counter:
    Print("Invalid initial state\n");
    return 1;
  ;

  // Setting the initial state of the automaton
  ok = write instance <- init_state;
  if not ok:
    Print("Invalid initial state\n");
    return 1;
  ;

  // Reading and checking the message list
  res = ReadValueFromFile(msg_list_fname);
  return 1 if res == nothing;
  msg_list = value(res);
  if not msg_list :: CounterMsg*:
    Print("Invalid message list\n");
    return 1;
  ;

  // Sending all messages in the list
  for msg @ i <- msg_list:
    ok = instance <- msg;
    if not ok:
      Print("Message number " & _print_(i) & " failed\n");
    ;
  ;

  // Saving the final state
  final_state = read instance;
  ok = FileWrite(final_state_fname, untag(_print_(final_state)));
  if not ok:
    Print("Could not write to file " & final_state_fname & "\n");
    return 1;
  ;

  return 0;
}

Maybe[Any] ReadValueFromFile(String fname) {
  res = FileRead(fname);
  if res == nothing:
    Print("Cannot read file " & fname & "\n");
    return nothing;
  ;

  res = _parse_(string(value(res)));
  if failed(res):
    Print("File " & fname & " does not contain a valid Cell value\n");
    return nothing;
  ;

  return just(result(res));
}

The first line in the body of Main(..) is the declaration of the automaton variable instance, which looks like an ordinary variable declaration. Automaton variables are instantiated and initialized as soon as the procedure that hosts them is called, and their initial state is the one that is provided with the schema declaration, which in the case of Counter is just (value: 0, updates: 0).

The first step is to load the initial state for counter from the given file, check that it's a valid one using the runtime type check init_state :: Counter and set the state of instance with the command:

ok = write instance <- init_state;

ok is a boolean variable that indicates whether the operation succeeded. Generally speaking, setting the state of an automaton instance can fail if the state that is provided is not a valid one. The typechecker tries to prevent you from using an invalid state in the first place, and that's why the init_state :: Counter check is actually necessary, but it doesn't verify that integrity constraints (which just means mutable relation variables' keys at the moment) are actually met, since that's rather hard to do with just a static analysis of the code, so those constraints are checked only when you actually try to set the state of an automaton instance.

The state of any automaton can be set at any time, any number of times. It's just like setting the value of a variable of an atomic type (like booleans, integers or floating point numbers) in any other language. The next step is to load the list of messages and send them in the given order to instance with the instruction:

ok = instance <- msg;

Here too the variable ok indicates whether the message was processed successfully. Also note the msg_list :: CounterMsg* check, which is required to verify that whatever data was loaded from the input file was indeed a valid sequence of messages for Counter.

The last instruction we have to manipulate relational automata is used to take a snapshot of the state of an automaton instance:

final_state = read instance;

As already explained in the previous chapters the state of an automaton cannot be aliased in any way, so making a copy of it requires making a physical copy of at least some of the underlying data structures that are used to store it. How much data exactly has to be copied depends on the implementation and the target language, but it generally is a rather expensive operation, especially if the automaton contains mutable relation variables. In the worst case, the entirety of the data structures that encode its state will have to be physically copied.

Reactive automata

To see how to use reactive automata, we'll write some test cases for some of the automata we defined earlier. For our first example that we'll make use of Switch, which only uses continuous signals and is not time-aware:

// The first two columns are the values of the switch_on
// and switch_off inputs respectively, and the third one
// is the expected value of the is_on output, encoded as
// nothing if the signal is expected to be undefined, or
// just(b) if its value is expected to be b
(Bool, Bool, Maybe[Bool])* switch_test_data = (
  (false,  false,  just(false)),
  (true,   false,  just(true)),
  (false,  true,   just(false)),
  (true,   true,   nothing),
  (true,   false,  just(true)),
  (false,  false,  just(false))
);

Main(String* args) {
  switch : Switch;

  for switch_on, switch_off, exp_is_on <- switch_test_data:
    // Setting the new values of the inputs for the next
    // propagation step. Internal state and outputs are
    // not affected at this stage.
    switch.switch_on = switch_on;
    switch.switch_off = switch_off;

    // Propagation step. The values of all outputs, state
    // variables and other internal signals is updated here.
    done = apply switch;

    // Now checking that the state of the
    // only output is the expected one
    if exp_is_on == nothing:
      // Here we expect is_on to be undefined
      if switch.is_on??:
        Print("Error: output was supposed to be undefined\n");
        return;
      ;
    else
      // First we check is_on is defined
      if not switch.is_on??:
        Print("Error: output is not defined\n");
        return;
      ;
      // Now we check its value is what we expected
      if value(exp_is_on) != switch.is_on:
        Print("Error: unexpected output value\n");
        return;
      ;
    ;

    Print("OK\n");
  ;
}

The first thing you need to do with a new automaton instance is to set the value of all its continuous inputs. A failure to set any of them will be treated as a runtime error: the input will be left in an undefined state, which will be then propagated to all other signals that depend on it. At this stage, you should not try to set any discrete inputs, as that can be done only once the automaton has been initialized.

Once the inputs are set it's time to initialize the instance. That's done with the apply statement, whose parameter is the name of the automaton variable to initialize, and whose return value can be safely ignored here since it's meaningful only for time-aware automata. The same apply statement is also used both to initialize the automaton and to propagate input changes, but there are significant differences between the two operations. As explained before, in the former case all continuous derived signals are initialized, state variables are set to the value provided with their declaration but their update rules are ignored, and discrete signals are ignored as well.

Once the automaton instance has been initialized, you'll be able to check the state of the outputs. You can read them using the familiar instance.output syntax, but keep in mind that trying to read the value of an undefined output will result in an exception that will terminate the program. Inside a reactive automaton you don't need to worry about that because errors are propagated automatically, but outside that particular context you need to explicitly check whether an output is defined before reading its value if you want to avoid errors. That's done using the instance.output?? expression, which returns true if the output is defined or false otherwise.

Once the automaton is initialized its life becomes a cycle where you update its inputs when needed, propagate those updates throughout the automaton and then check how the outputs have changed and react accordingly. Keep in mind that just setting the values of the inputs does not trigger the update propagation process, which has to be done explicitly using the apply statement.

Taking a snapshot of and restoring the state of a reactive automaton is the same as doing it with a relational one, using the read and write statements respectively. The first command saves the values of all continuous inputs and state variables, but not the timers. If the automaton that does not contain any timed rules its state can be reconstructed exactly later; otherwise timed rules will behave as if all signals have no previous history.

Let's now see an example of how to deal with discrete signals using another automaton we've already seen before, Lines, which splits a string of characters into lines. We'll use it to split a test strings, and we'll print the results:

Main(String* args) {
  lines : Lines;

  // Initializing the automaton variable lines
  done = apply lines;

  // Multiline string used as a test input
  str = "line 1\nline 2\nline 3\nline4\n";

  // Feeding the input characters into the automaton
  for ch <- untag(str):
    lines.char = ch;
    done = apply lines;
    // If the output line is active, we just print it
    if lines.line?:
      Print(lines.line & "\n");
    ;
  ;
}

Here the automaton instance is initialized before any input is set. That's because only continuous inputs should be set before initialization, and Lines has none. Once initialized, the automaton is fed characters from a test string. That's done in the first two lines of the loop. After each input character is processed we check to see if the line output is active and if it is we just print it. Checking whether a discrete output is active is syntactically similar to checking if it's defined, but with only one question mark at the end instead of two: instance.discrete_output?. Trying to read the value of a discrete output that is dormant has the same effect as trying to read an output that is in an undefined state: it triggers an exception that terminates the program. So in general in order to safely read the value of a discrete output you first have to check whether it's defined with instance.discrete_output?? (this step was omitted in the example because we assumed line could never be undefined), then check if it's set with instance.discrete_output? and only after that you can safely read its value (with continuous outputs the second step is of course not necessary).

Time-aware reactive automata

The process of updating an instance of a reactive automaton is a bit more complex for reactive automata that contains timed rules or contains other automata that use timed rules. Here's an example:

// The first field is the reading from the sensor
// The second one is the time that has passed since the last
// reading, or since initialization for the first reading
// The third one is the sequence of values sensor_state is
// expected to have after each update step
(Maybe[Bool], Nat, WaterSensorState+)* water_sensor_test_data = (
  (just(false), 40000, (:unknown, :submerged(false))),
  (nothing,     10000, (:submerged(false))),
  (nothing,     10000, (:submerged(false))),
  (nothing,     10000, (:unknown)),
  (just(true),  10000, (:submerged(true))),
  (just(false), 50000, (:unknown, :submerged(false)))
);

Main(String* args) {
  water_sensor : WaterSensor;

  // Initialization
  done = apply water_sensor;

  for reading, time, exp_states <- water_sensor_test_data:
    // Setting the value of the only input
    water_sensor.raw_reading = reading;

    // Setting the amount of time that has passed since
    // the last update, or since the automaton was started
    elapsed water_sensor time;

    // Updating water_sensor and recording all
    // the intermediate values of the only output
    states = ();
    loop
      done = apply water_sensor;
      states = (states | water_sensor.sensor_state);
    while not done;

    // Checking that the states of the sensor are
    // the expected ones
    if states != exp_states:
      Print("Error\n");
      return;
    else
      Print("OK\n");
    ;
  ;
}

The elapsed command is used to provide the time information. Reactive automata don't actively try to keep track of time: instead, time is treated more like a sort of implicit input (albeit one with very special characteristics) that the client has to explicitly set before updating an automaton instance with apply. The first argument of elapsed is an automaton instance, and the second one is the number of milliseconds that have passed since the last time the instance was updated. If you don't explicitly provide that piece of information the internal clock of the automaton is not updated, and from the automaton perspective it's as if no time at all had passed since the last update. Note that you don't have to and actually cannot use the elapsed command before an automaton instance is initialized, as initialization is regarded as time zero.

The other difference with automata that are not time-aware is that the apply command has to be called repeatedly until it returns true. In order to understand why, consider what would happen when applying the test inputs defined by water_sensor_test_data. The automaton receives the first sensor reading after 40 seconds of simulated time, but the rule that sets sensor_state to unknown is supposed to be triggered 10 seconds before that. So the first thing the automaton has to do when the apply command is executed is to catch up on all the backlog. It sets the internal clock forward by 30 seconds, the time when the first (and only, in this case) timer expires, and sets sensor_state to unknown. At that point, that is, after 30 seconds of simulated time, before even processing the new input the apply command finishes and returns false. It does so in order to give its client a chance to react to the first time-triggered update. After that the client is expected to call the apply command as many times as needed, until all expired timers have been processed. Once all timers have been taken care of the automaton processes the new inputs, which finally completes the update, and returns true.

In a real application of course you're supposed to periodically update a time-aware automaton, even when no inputs have changed, in order to allow the timed rule to update its state in real time. But the behaviour of the automaton is always deterministic: whenever you give it a chance to update its state, it always completes all pending updates before processing the new inputs.