Developer Guidelines

PINS Extensions

We can use this wiki to track POR extensions that will ultimately require PINS redesign to improve the coherency of the introduced features.

Basic PINS

PINS assumes a few things:
  • Every states in the model have the same length.
  • Every transition in the model has the same number of labels.
  • The types of labels are the same for each transition.
This is reflected by the LTStype definition, which maintains inter-alia:
  • State length L and names/types of the L slots
  • Action labels (Fixed)
PINS consists of:
  • next-state functions: S --> (S, Group), S X Group --> S (extended with actions)
  • state-label function: S X Label --> Boolean
  • transition label function: S X Action --> String
  • Dependency matrices: READ, WRITE, DEPENDENT: Slot X Group --> Boolean

PINS2PINS wrappers

(Higher)
Algorithm
---------
LTL
---------
POR
---------
Caching
---------
Language frontend
(Lower)

Timed Automata Extensions

TODO

POR Extensions

To enable POR, PINS was extended with, for detail refer to Elwin Pater's Thesis:
  • Transition guards: Group --> Guard*, with Guard \subset Label
  • Maybe-Coenabled Matrix: Guard X Guard --> Boolean
  • (Optional) Necessary Enabling Matrix: Guard X Group --> Boolean
  • (Optional) Necessary Disabling Matrix: Guard X Group --> Boolean

To distinguish guards from other state labels, state label groups we introduced.

POR LTL extension

To enable POR with LTL, the algorithmic backend needs a slight coupling to the POR PINS2PINS wrapper. To this end, the transition_info struct, which is used to provide information on the successor states was extended. The basic struct passes the following items to the algorithm together with the state:

  1. Group index: Group
  2. Action labels: Action -> String (not included in next state function)

To pass information from the algorithms to the PINS POR wrapper, the following was added:

  1. Por proviso: Boolean

Additionally a the group visibility is exported as an array:

  • Group visibility: Group --> Boolean

Space for this array is reserved by the POR PINS wrapper (GBsetPorGroupVisibility) and the information is provided by the higher LTL PINS wrapper by deducing which group's enabledness depends on the variables in the LTL formula. The variables refer to state slots, and can thus mapped to the groups via the dependency matrix.

The accepting state property is exported as another reserved state label (see GBgetAcceptingStateLabelIndex).

Promela Extensions

Promela introduces a few unique modeling concepts: valid end states that are not to be counted as deadlocks, and progress states, which are those states that can execute a progress statement in the model (a statement marked with a specific label).

The progress and valid-end state property is exported as reserved state label (see GBgetProgressStateLabelIndex and GBgetValidEndStateLabelIndex).

To export the line numbers in the Promela code for tracing, a dedicated action label "statement" was introduced (see ltsmin-lib/ltsmin-standard.h).

POR Improvements (by Alfons)

To refine the visibility, we allow state labels (including guards) to be used in the definition of an LTL formula. An additional state label visibility matrix:
  • State label visibility: Label X Group --> Boolean

This way, the visibility of the LTL formula can again be mapped to the transition groups.

DFS_FIFO Extensions

DFS_FIFO can use progress transitions instead of progress states to check for livelocks (see DFS_FIFO). These can be statically identified, i.e. ProgressTrans \subset Group.
To distinguish the subset of groups that make progress, we require the "statement" action label (see Promela Extensions) to contain exactly one string value per group. Progress groups are identified by string values that contain "<progress>" (see ltsmin-lib/ltsmin-standard.h).

Priority Extensions

TODO

Proposed changes

  • Replace Visibility matrix by pacing state labels in LTL formula to POR layer which can use NES / NDS (state-based).
  • The PINS stack adds labels to the state (guard for POR) and to the edges (prioritisation/tau confluence). These can be filtered when writing to disk using the default filter of the model. I would be possible extend the filter family with functions to filter certain edge labels groups, etc.
  • Static information matrices should not be hardcoded into the PINS API. Instead the PINS APS should allow static information matrices to be added in such a way that common wrappers, like grouping and caching know how to preserve and/or recompute them.
  • Define a means to identify subsets of groups, like DFS_FIFO's (SPIN's) progress transitions
  • Move state allocation to the algorithmic backends:
    • GBgetTransitionsAll (model_t model, int *src, int **tgt)
      An implementation of the callback could be:
      void callback (context *ctx, transition_info_t *ti, int **tgt) {
          if (!table_has(ctx->table, *tgt))
              *tgt = stack_push (ctx->stack) // reserve room for next
          (void) ti;
      }
      void main() {
          int *tgt = stack_push (ctx->stack);// reserve room for first
          GBgetTransitionsAll (model_t model, int *src, &tgt, callback, ctx)
      }
      
    • transition_info_t now contains:
      struct transition_info_t {
          /* Note that both the edge_labels and dest pointers
             may be changed by the callback. For example, if
             edges are inserted into a list. */
          int *edge_labels;
          int *dest;
          int group;
          int por_proviso;
      }
      

      These should all be allocated at the algorithmic backend as well.