build_jani_model

build_jani_model(
gspn: GSPN,
*,
automaton_name: str = 'gspn_automaton',
add_deadlock_properties: bool = False,
) → tuple[JaniModel, list[Property]]

Translate a GSPN into a JANI model.

Parameters:

  • gspn – GSPN.

  • automaton_name – Name of the JANI automaton.

  • add_deadlock_properties – Whether to create the standard properties for deadlocks (reachability, time-bounded reachability with the constant TIME_BOUND, and expected time). This adds transient variables for deadlocks to the model.

Returns:

The JANI model and the deadlock properties (empty if not requested).