This lesson explains print output by means of examples. It does not explain all uses of print output, and all details related to print output. For those details, see the reference manual’s print declarations documentation instead.

In this lesson, only the output from print declarations is shown when console output is presented. All other output, such as that from the CIF simulator, is omitted.

Before we start with the examples, there is a section that introduces the example model and trace on which the examples are based. Then, the following examples are explained in detail:

Example model and trace

The examples of print output in this lesson all make use of the same CIF model:

automaton buffer:
  event add, remove;
  disc int cnt = 5;

  location:
    initial;
    edge add    when cnt < 10 do cnt := cnt + 1;
    edge remove when cnt >  0 do cnt := cnt - 1;
end

The buffer initially contains five items (cnt = 5). As long as there is room in the buffer (cnt < 10), an item can be added (event add) to the buffer. As long as the buffer is not empty (cnt > 0), an item can be removed (event remove) from the buffer. The model allows to choose between adding an item to the buffer, and removing an item from the buffer. The following is a potential simulation/execution trace:

trace normal

In the initial state (S1), variable cnt has value 5. An item is then added (transition for the event add), resulting in a new state (S2), where cnt has value 6. After that, another item is added, leading to state S3, where cnt has value 7. Finally, an item is removed by means of a transition for event remove, leading to state S4, where cnt has value 6 again.

Example 1: Printing the buffer count for all states

If we want to print for every state (S1 through S4), the number of items in the buffer, we could add the following print declaration to automaton buffer:

print cnt;

Then, as a result of this print declaration, the following text is printed to the console:

5
6
7
6

That is, for every state (S1 through S4), the value of variable cnt is printed, on a new line.

Example 2: Printing to a file

Consider the following print declarations:

print cnt     file "a.txt";
print cnt * 2 file "b.txt";

The first print declaration results in the number of items in the buffer being printed for every state of the trace, to a file named a.txt. The second print declaration prints the number of items in the buffer multiplied by two, to a file named b.txt. These declarations use local file declarations to specify the file to which output is to be written. It is also possible to use global print file declarations:

printfile "ab.txt";
print cnt;
print cnt * 2;

The print file declaration declares that output of this scope is to be printed to a file named ab.txt. The two print declarations don’t specify a local file declaration, and thus use the default file for their scope, in this case file ab.txt. Alternating lines with the number of items in the buffer and twice that amount are thus printed to that file.

Example 3: Printing the odd/even status for all states

If we want to print for every state, whether the buffer contains an odd or even number of items, we could add the following print declaration to automaton buffer:

print if cnt mod 2 = 0: "even" else "odd" end;

The print declaration uses an if expression. Then, as a result of this print declaration, the following text is printed to the console:

odd
even
odd
even

Example 4: Printing only for odd states

If we want to print the number of items in the buffer, but only for states where the number of items is odd, we could add the following print declaration to automaton buffer:

print cnt when cnt mod 2 = 1;

Then, as a result of this print declaration, the following text is printed to the console:

5
7

Example 5: Printing the result of adding an item

If we want to print the result of adding an item, that is the new buffer count after a transition for the add event, we could add the following print declaration to automaton buffer:

print cnt for add;

Then, as a result of this print declaration, the following text is printed to the console:

6
7

Since twice an item is added to the buffer, two lines of text are printed.

Example 6: Printing addition/removal results

If we want to print the resulting buffer count after every change to the buffer (addition or removal), we could add the following print declaration to automaton buffer:

print cnt for add, remove;

Then, as a result of this print declaration, the following text is printed to the console:

6
7
6

Two items are added to the buffer, and one item is removed from the buffer, leading to three lines of text being printed.

Since the add and remove events are the only events in the system, and no edges exist without an event (which would implicitly use the tau event), the print declaration can also be specified as follows:

print cnt for event;

That is, the value of variable cnt is printed after each event transition.

Example 7: Printing value changes

If we want to print the buffer count before and after removal of an item from the buffer, we could add the following print declaration to automaton buffer:

print pre cnt post cnt for remove;

As a result of this print declaration, the following text is printed to the console:

7
6

As only one item is removed for our example trace, two lines of text are printed, one with the buffer count before the removal (due to pre cnt), and one with the buffer count after the removal (due to post cnt).

Example 8: Printing headers and footers

If we want to print for every state (S1 through S4), the number of items in the buffer, we could add the following print declaration to automaton buffer:

print cnt;

If we want to print some text before this, as a header, and some text after this, as a footer, we could add the following print declaration to the top level scope of the specification, or to automaton buffer:

print "header" for initial;
print "footer" for final;

As a result of the original print declaration, and these two new print declarations, the following text is printed to the console:

header
5
6
7
6
footer

Example 9: Printing the new time after time passes

In the example trace given at the top of this page, no passage of time is included. If however a trace includes time passage, it is possible to filter printing to only time transitions. For instance, if we want to print the new time after time passes, we could use the following print declaration:

print time for time;

This prints the value of variable time, every time after a time transition. The first time in the print declaration denotes that the value of variable time should be printed, and the second time denotes that it should be printed only after passage of time (after time transitions). As an example, the following could be printed to the console:

0.005
0.75
3.1
7.9

Example 10: Printing all unique time values

In the ninth example, we printed the new time value after each time transition. However, initially time is zero. Since the initial state is not reached via a time transition, time zero is not printed. We could adapt the print declaration to the following, to print all unique values of variable time, for all states of the trace:

print time for initial, time;

This initially prints the value of variable time, and also prints it after every time transition. As an example, the following could be printed to the console:

0.0
0.005
0.75
3.1
7.9

Example 11: Printing transitions to/from a location

In the example model given at the top of this page, automaton buffer has only one location. If however an automaton has multiple locations, it may be useful to print the effect of transitions ending in a certain location, or the state of the system for transitions starting in a certain location. Consider the following print declaration:

print x for event when aut.loc;

This prints the value of variable x after event transitions leading to a state where location loc is the current location of automaton aut. That is, whenever an event transition leads to entering that location, the value of variable x after that transition is printed. Since self loops have the same source and target location, this includes self loops. To exclude self loops, use the following print declaration:

print x for event when pre not aut.loc post aut.loc;

This print declaration prints the same text, but only prints it after event transitions from a state where location loc is not the current location of automaton aut to a state where location loc is the current location of automaton aut.

So far in this example, we printed text for transitions ending in a location. To print text for transitions starting in a location, consider the following print declaration:

print pre y for event when pre aut.loc post not aut.loc;

This print declaration prints the value of variable y in the state that is exited by the transition, for all event transitions that start in location loc of automaton aut, but do end in that same location.