Configuring time diagrams

Once a time diagram has been constructed you can configure what information should be displayed. This helps to filter out uninteresting data.

To select which places' token numbers should be visualized in the diagram choose the menu item Select places from the Configure menu. This will open the window shown below.

Place selection window

In this window you can select the places by checking the check boxes on their rows. To quickly select or deselect all places in the table right-click on the table to bring up a popup menu. Then select either Select all places or Deselect all places from the menu. Clicking on the Select button closes the window and enforces the selections on the diagram. You can also click on the Cancel button to close the window and invalidate any change to the selections.