mCRL2

https://mcrl2.org/web/
Admin
mCRL2 is a formal specification and verification toolset for modeling and analyzing concurrent...
Tokens:31,469,323
Snippets:157,924
Trust Score:8.1
Update:9 months ago
Show doc for...
Tokens:
Raw
### Generate Counterexample for ABP Protocol (LTS)

Source: https://mcrl2.org/web/user_manual/tools/release/pbessolve

This example shows how to generate a counterexample for the ABP protocol property starting from an LTS file. It involves converting the specification to LPS, then to LTS, then to PBES with counterexample information, solving the PBES, and visualizing the counterexample LTS. Similar to the LPS example, the -c and --file options are important for generating counterexamples.

```bash
mcrl22lps abp.mcrl2 abp.lps
lps2lts abp.lps abp.lts
lts2pbes -v -c -f infinitely_often_enabled_then_infinitely_often_taken.mcf abp.lts abp.pbes
pbessolve -v --file=abp.lts abp.pbes
ltsgraph abp.pbes.evidence.lts
```

--------------------------------

### Counter Example Construction API

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1dummy__counter__example__constructor

This API allows for the construction and saving of counter examples. It provides methods to add transitions, save the counter example to a file or stdout, and retrieve the corresponding trace.

```APIDOC
## POST /counter_example/add_transition

### Description
Adds a transition to the counter example being constructed.

### Method
POST

### Endpoint
/counter_example/add_transition

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **state_index** (size_t) - Required - The index of the state.
- **next_index** (index_type) - Required - The index of the next state or transition.

### Request Example
```json
{
  "state_index": 0,
  "next_index": 1
}
```

### Response
#### Success Response (200)
- **new_index** (index_type) - The index of the added transition or state.

#### Response Example
```json
{
  "new_index": 2
}
```

## POST /counter_example/save

### Description
Saves the constructed counter example. It can be saved to a file or printed to stdout.

### Method
POST

### Endpoint
/counter_example/save

### Parameters
#### Path Parameters
None

#### Query Parameters
- **output_target** (string) - Optional - Specifies where to save the counter example. "stdout" for printing to standard output, or a file path. Defaults to stdout.

#### Request Body
- **root_index** (index_type) - Required - The index of the root of the counter example.
- **lts_data** (object) - Required - The LTS data structure.
- **state_indices** (array of size_t) - Optional - A vector of state indices to include in the counter example.

### Request Example
```json
{
  "root_index": 0,
  "lts_data": { ... },
  "state_indices": [0, 1, 2]
}
```

### Response
#### Success Response (200)
- **status** (string) - Indicates the success of the save operation.

#### Response Example
```json
{
  "status": "Counter example saved successfully."
}
```

## GET /counter_example/trace

### Description
Retrieves the trace associated with a given counter example.

### Method
GET

### Endpoint
/counter_example/trace

### Parameters
#### Path Parameters
None

#### Query Parameters
- **lts_data** (object) - Required - The LTS data structure.
- **index** (index_type) - Required - The index of the counter example.

### Request Example
```
/counter_example/trace?lts_data={...}&index=0
```

### Response
#### Success Response (200)
- **trace_data** (trace) - The trace object representing the counter example.

#### Response Example
```json
{
  "trace_data": { ... }
}
```

## GET /counter_example/is_dummy

### Description
Checks if the counter example is a dummy, meaning no counter example is required.

### Method
GET

### Endpoint
/counter_example/is_dummy

### Parameters
None

### Response
#### Success Response (200)
- **is_dummy** (boolean) - True if it's a dummy counter example, false otherwise.

#### Response Example
```json
{
  "is_dummy": true
}
```

## GET /counter_example/is_structured

### Description
Returns whether this counter-example is printed in a machine-readable way to stdout.

### Method
GET

### Endpoint
/counter_example/is_structured

### Parameters
None

### Response
#### Success Response (200)
- **is_structured** (boolean) - True if the counter-example is structured for machine readability, false otherwise.

#### Response Example
```json
{
  "is_structured": true
}
```

## GET /counter_example/root_index

### Description
Retrieves the index for the root of a counter example.

### Method
GET

### Endpoint
/counter_example/root_index

### Parameters
None

### Response
#### Success Response (200)
- **root_index** (index_type) - The index representing the root of the counter example.

#### Response Example
```json
{
  "root_index": 0
}
```
```

--------------------------------

### Initialization and Setup Functions

Source: https://mcrl2.org/web/doxygen/functions_func_i

Functions for initializing various components and data structures.

```APIDOC
## init()

### Description
Initializes various mCRL2 components, including checks, traces, algorithms, and process specifications.

### Method
GET

### Endpoint
/websites/mcrl2_web/init

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message indicating successful initialization.

#### Response Example
```json
{
  "status": "Initialization successful."
}
```
```

```APIDOC
## init_allowed_actions()

### Description
Initializes allowed actions for communication algorithms.

### Method
GET

### Endpoint
/websites/mcrl2_web/init_allowed_actions

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **result** (mcrl2::lps::detail::apply_communication_algorithm) - The result of initializing allowed actions.

#### Response Example
```json
{
  "result": "..."
}
```
```

```APIDOC
## init_lhs()

### Description
Initializes the left-hand side of a communication entry.

### Method
GET

### Endpoint
/websites/mcrl2_web/init_lhs

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **comm_entry** (mcrl2::lps::detail::comm_entry) - The initialized communication entry (LHS).

#### Response Example
```json
{
  "comm_entry": "..."
}
```
```

```APIDOC
## init_node()

### Description
Initializes a node within a probabilistic bisimulation partitioner tree.

### Method
GET

### Endpoint
/websites/mcrl2_web/init_node

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **tree_node** (mcrl2::lts::detail::prob_bisim_partitioner_bem::tree_type) - The initialized tree node.

#### Response Example
```json
{
  "tree_node": "..."
}
```
```

```APIDOC
## init_rhs()

### Description
Initializes the right-hand side of a communication entry.

### Method
GET

### Endpoint
/websites/mcrl2_web/init_rhs

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **comm_entry** (mcrl2::lps::detail::comm_entry) - The initialized communication entry (RHS).

#### Response Example
```json
{
  "comm_entry": "..."
}
```
```

```APIDOC
## init_transitions()

### Description
Initializes transitions for the BGSKW bisimulation algorithm.

### Method
GET

### Endpoint
/websites/mcrl2_web/init_transitions

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **helper** (mcrl2::lts::detail::bisim_gjkw::bisim_partitioner_gjkw_initialise_helper) - The transition initialization helper.

#### Response Example
```json
{
  "helper": "..."
}
```
```

```APIDOC
## initial_probabilistic_state()

### Description
Retrieves the initial probabilistic state of a probabilistic LTS.

### Method
GET

### Endpoint
/websites/mcrl2_web/initial_probabilistic_state

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **state** (mcrl2::lts::probabilistic_lts) - The initial probabilistic state.

#### Response Example
```json
{
  "state": "..."
}
```
```

```APIDOC
## initial_process()

### Description
Retrieves the initial process of a specification.

### Method
GET

### Endpoint
/websites/mcrl2_web/initial_process

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **process** (mcrl2::lps::specification_base) - The initial process.

#### Response Example
```json
{
  "process": "..."
}
```
```

```APIDOC
## initial_state()

### Description
Retrieves the initial state of various mCRL2 models (LPS, LTS, PBES, PRES).

### Method
GET

### Endpoint
/websites/mcrl2_web/initial_state

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **state** (mcrl2::lps::explorer | mcrl2::lts::lts | mcrl2::lts::probabilistic_lts | mcrl2::pbes_system::detail::pfnf_pbes | mcrl2::pbes_system::detail::pre_srf_pbes | mcrl2::pbes_system::detail::stategraph_pbes | mcrl2::pbes_system::explorer | mcrl2::pbes_system::partial_order_reduction_algorithm | mcrl2::pbes_system::pbes | mcrl2::pres_system::pres) - The initial state.

#### Response Example
```json
{
  "state": "..."
}
```
```

```APIDOC
## initial_vertex()

### Description
Retrieves the initial vertex of a structure graph.

### Method
GET

### Endpoint
/websites/mcrl2_web/initial_vertex

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **vertex** (mcrl2::pbes_system::detail::structure_graph_builder | mcrl2::pbes_system::structure_graph) - The initial vertex.

#### Response Example
```json
{
  "vertex": "..."
}
```
```

```APIDOC
## initialise()

### Description
Initializes an iterator for a term balanced tree.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **iterator** (atermpp::term_balanced_tree::iterator) - The initialized iterator.

#### Response Example
```json
{
  "iterator": "..."
}
```
```

```APIDOC
## initialise_datastructures()

### Description
Initializes data structures for the simulation partitioner.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise_datastructures

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message.

#### Response Example
```json
{
  "status": "Data structures initialized."
}
```
```

```APIDOC
## initialise_Pi()

### Description
Initializes Pi for the simulation partitioner.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise_Pi

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message.

#### Response Example
```json
{
  "status": "Pi initialized."
}
```
```

```APIDOC
## initialise_pre_EA()

### Description
Initializes pre-EA for the simulation partitioner.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise_pre_EA

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message.

#### Response Example
```json
{
  "status": "pre_EA initialized."
}
```
```

```APIDOC
## initialise_Sigma()

### Description
Initializes Sigma for the simulation partitioner.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise_Sigma

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message.

#### Response Example
```json
{
  "status": "Sigma initialized."
}
```
```

```APIDOC
## initialise_system_defined_functions()

### Description
Initializes system-defined functions for data type checking.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialise_system_defined_functions

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **checker** (mcrl2::data::data_type_checker | mcrl2::data::type_checker) - The initialized type checker.

#### Response Example
```json
{
  "checker": "..."
}
```
```

```APIDOC
## initialize()

### Description
Performs general initialization for various mCRL2 components, including induction, transition structures, and SMT solvers.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialize

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **status** (string) - Confirmation message indicating successful initialization.

#### Response Example
```json
{
  "status": "General initialization successful."
}
```
```

```APIDOC
## initialize_generation()

### Description
Initializes the parity game generator.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialize_generation

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **generator** (mcrl2::pbes_system::parity_game_generator) - The initialized parity game generator.

#### Response Example
```json
{
  "generator": "..."
}
```
```

```APIDOC
## initialize_lifting_strategy()

### Description
Initializes the lifting strategy for small progress measures.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialize_lifting_strategy

### Parameters
None

### Request Example
```json
{}
```

### Response
#### Success Response (200)
- **strategy** (SmallProgressMeasures) - The initialized lifting strategy.

#### Response Example
```json
{
  "strategy": "..."
}
```
```

```APIDOC
## initialize_loops()

### Description
Initializes loop detection for small progress measures.

### Method
GET

### Endpoint
/websites/mcrl2_web/initialize_loops

### Parameters
None

### Request Example
```json
{}
```

### Response
```

--------------------------------

### Get Counter Example Index from Triple

Source: https://mcrl2.org/web/doxygen/lts__convert_8h_source

Retrieves the counter example index from a `state_states_counter_example_index_triple`. This is a const member function.

```cpp
const COUNTER_EXAMPLE_CONSTRUCTOR::index_type & counter_example_index() const

```

--------------------------------

### PBES Instantiation Details

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1propositional__variable__instantiation-members

Detailed algorithms and options for instantiating PBES, covering various approaches like finite, lazy, and symbolic instantiation, as well as counter-example generation.

```APIDOC
## PBES Instantiation Details

### Description
Provides a comprehensive set of algorithms and options for instantiating PBES. This includes different instantiation strategies (finite, lazy, symbolic) and methods for generating counter-examples.

### Endpoints

*   **pbesinst_alternative_lazy_algorithm**
    *   **Description**: Alternative lazy instantiation algorithm for PBES.
    *   **Method**: (Not specified)

*   **pbesinst_counter_example_structure_graph_algorithm**
    *   **Description**: Algorithm to generate a counter-example structure graph from PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_counter_example_structure_graph_algorithm2**
    *   **Description**: Second version of the algorithm for generating counter-example structure graphs.
    *   **Method**: (Not specified)

*   **pbesinst_finite_rename**
    *   **Description**: Renaming utility for finite PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_lazy_todo**
    *   **Description**: Manages the 'to-do' list for lazy PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_rename**
    *   **Description**: Renaming utility for PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_rename_long**
    *   **Description**: Renaming utility for long identifiers in PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_structure_graph_algorithm**
    *   **Description**: Algorithm to generate a structure graph from PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_structure_graph_algorithm2**
    *   **Description**: Second version of the algorithm for generating structure graphs from PBES instantiation.
    *   **Method**: (Not specified)

*   **pbesinst_symbolic_algorithm**
    *   **Description**: Algorithm for symbolic instantiation of PBES.
    *   **Method**: (Not specified)

### Parameters
(No specific parameters detailed for these instantiation functions.)

### Request Example
(No request examples provided for these functions.)

### Response
(No specific response details provided for these functions.)
```

--------------------------------

### Get Counter Example Index (COUNTER_EXAMPLE_CONSTRUCTOR)

Source: https://mcrl2.org/web/doxygen/counter__example_8h_source

Retrieves the counter example index from the COUNTER_EXAMPLE_CONSTRUCTOR. This is likely used in debugging or analysis tools to identify specific counter-examples. It returns an index_type.

```cpp
const COUNTER_EXAMPLE_CONSTRUCTOR::index_type & counter_example_index() const
Get the counter example index.
```

--------------------------------

### create_initial_partition_gjkw()

Source: https://mcrl2.org/web/doxygen/functions_c

Creates an initial partition using the GJKW algorithm.

```APIDOC
## create_initial_partition_gjkw()

### Description
Creates an initial partition using the GJKW algorithm.

### Method
N/A

### Endpoint
N/A

### Parameters
N/A

### Request Example
N/A

### Response
N/A

### Response Example
N/A
```

--------------------------------

### Get start symbol from parser_table (C++)

Source: https://mcrl2.org/web/doxygen/dparser__functions_8h_source

Retrieves the integer identifier for a start symbol at a given index. This is used to define the entry points for parsing.

```cpp
int mcrl2::core::parser_table::start_symbol(unsigned int i) const
```

--------------------------------

### Get start symbol index by name (C++)

Source: https://mcrl2.org/web/doxygen/dparser__functions_8h_source

Retrieves the index of a start symbol given its name. This is a convenience function that likely uses the underlying `parser_table`.

```cpp
unsigned int mcrl2::core::parser::start_symbol_index(const std::string &name) const
```

--------------------------------

### create_initial_partition__set_start_incoming_transitions

Source: https://mcrl2.org/web/doxygen/functions_c

Sets start incoming transitions in initial partition, likely for complexity checking.

```APIDOC
## create_initial_partition__set_start_incoming_transitions

### Description
Sets start incoming transitions.

### Method
N/A

### Endpoint
N/A

### Parameters
N/A

### Request Example
N/A

### Response
N/A

### Response Example
N/A
```

--------------------------------

### Get Root Index of Counter Example

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1counter__example__constructor

Returns the index of the root node in the counterexample tree. This is a static function.

```cpp
static index_type mcrl2::lts::detail::counter_example_constructor::root_index()
```

--------------------------------

### bisim_partitioner_gjkw_initialise_helper()

Source: https://mcrl2.org/web/doxygen/group__part__refine

Constructor for the bisim_partitioner_gjkw_initialise_helper class.

```APIDOC
## POST /websites/mcrl2_web/bisim_partitioner_gjkw_initialise_helper

### Description
Constructor for the bisim_partitioner_gjkw_initialise_helper class.

### Method
POST

### Endpoint
/websites/mcrl2_web/bisim_partitioner_gjkw_initialise_helper

### Parameters
#### Request Body
- **_l_** (LTS_TYPE &) - Required - The LTS type.
- **_branching_** (bool) - Required - Whether to use branching bisimulation.
- **_preserve_divergence_** (bool) - Required - Whether to preserve divergence.

### Request Example
```json
{
  "_l_": { ... },
  "_branching_": true,
  "_preserve_divergence_": false
}
```

### Response
#### Success Response (200)
- **bisim_partitioner_gjkw_initialise_helper** - The constructed helper object.

#### Response Example
```json
{
  "helper": { ... }
}
```
```

--------------------------------

### PBES Instantiation Options and Algorithms

Source: https://mcrl2.org/web/doxygen/structmcrl2_1_1pbes__system_1_1no__strategy

This section details the various algorithms and options available for instantiating PBES, which is a key step in their analysis and solving.

```APIDOC
## PBES Instantiation Options and Algorithms

### Description
Provides a comprehensive set of algorithms and options for PBES instantiation.

### Endpoints

- `pbesinst_alternative_lazy_algorithm`
- `pbesinst_counter_example_structure_graph_algorithm`
- `pbesinst_finite_rename`
- `pbesinst_lazy_todo`
- `pbesinst_rename_long`
- `pbesinst_structure_graph_algorithm2`
- `pbesinst_symbolic_algorithm`

### Usage Examples

```javascript
// Example of using the finite rename instantiation algorithm
// mCRL2.pbesinst_finite_rename(pbes_spec, renaming_map);

// Example of using the lazy todo instantiation algorithm
// mCRL2.pbesinst_lazy_todo(pbes_spec);
```
```

--------------------------------

### Get start symbol index from parser_table by name (C++)

Source: https://mcrl2.org/web/doxygen/dparser__functions_8h_source

Finds the index of a start symbol given its string name. This allows parsing to begin from a specific named entry point in the grammar.

```cpp
unsigned int mcrl2::core::parser_table::start_symbol_index(const std::string &name) const
```

--------------------------------

### Generate Counterexample for ABP Protocol (LPS)

Source: https://mcrl2.org/web/user_manual/tools/release/pbessolve

This example demonstrates generating a counterexample for the 'infinitely often enabled then infinitely often taken' property of the ABP protocol starting from an LPS file. It involves converting the specification to LPS, then to PBES with counterexample information, solving the PBES, and visualizing the counterexample LTS. The -c option in lps2pbes and the --file option in pbessolve are crucial for counterexample generation.

```bash
mcrl22lps abp.mcrl2 abp.lps
lps2pbes -v -c -f infinitely_often_enabled_then_infinitely_often_taken.mcf abp.lps abp.pbes
pbessolve -v --file=abp.lps abp.pbes
lps2lts abp.pbes.evidence.lps abp.pbes.evidence.lts
ltsgraph abp.pbes.evidence.lts
```

--------------------------------

### Get State from Counter Example Triple

Source: https://mcrl2.org/web/doxygen/lts__convert_8h_source

Retrieves the state from a `state_states_counter_example_index_triple`. This is a const member function.

```cpp
state_type state() const

```

--------------------------------

### Initialize PBESSolver with Options

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1pbesinst__structure__graph__algorithm2

Constructors for the PBESSolver classes, initializing the algorithm with specified options, the PBES problem, a structure graph, and an optional rewriter. These constructors set up the necessary components for the solving process.

```cpp
pbesinst_structure_graph_algorithm2 (const pbessolve_options &options, const pbes &p, structure_graph &G, std::optional< data::rewriter > rewriter=std::nullopt)
```

```cpp
pbesinst_structure_graph_algorithm (const pbessolve_options &options, const pbes &p, structure_graph &G, std::optional< data::rewriter > rewriter=std::nullopt)
```

```cpp
pbesinst_lazy_algorithm (const pbessolve_options &options, const pbes &p, std::optional< data::rewriter > rewriter=std::nullopt)
```

--------------------------------

### Constructor for counter_example_constructor

Source: https://mcrl2.org/web/doxygen/lts__preorder_8h_source

Initializes a counter-example constructor with a name, counter-example file path, and a flag for structured output. It sets up the necessary internal state for building and storing counter-examples.

```cpp
mcrl2::lts::detail::counter_example_constructor::counter_example_constructor(const std::string &name, const std::string &counter_example_file, bool structured_output)
Constructor.

```

--------------------------------

### Get Trace from Counter Example

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1counter__example__constructor

Retrieves the trace from the root to a specified index within the counterexample. Requires an LTS object and the target index.

```cpp
template<class LTS_TYPE >
trace mcrl2::lts::detail::counter_example_constructor::get_trace(const LTS_TYPE& _l_, index_type _index_) const
```

--------------------------------

### Constructor for Counter Example

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1counter__example__constructor

Initializes a new instance of the counter_example class. It takes a name, a file path for counterexamples, and a boolean to indicate structured output.

```cpp
mcrl2::lts::detail::counter_example_constructor::counter_example_constructor(const std::string& _name_, const std::string& _counter_example_file_, bool _structured_output_)
```

--------------------------------

### Get Initial State for PBES Grey-box Interface

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1detail_1_1pbes__greybox__interface

Retrieves the initial state of the PBES, which has been rewritten and simplified. This is a core function for starting analysis.

```cpp
propositional_variable_instantiation mcrl2::pbes_system::detail::pbes_greybox_interface::get_initial_state() override
```

--------------------------------

### Create Initial Partition (C++)

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1bisim__partitioner__gj

Creates the initial partition of states. This is the starting point for the bisimulation refinement algorithm.

```cpp
void | create_initial_partition ()

```

--------------------------------

### Get Set of States from Counter Example Triple

Source: https://mcrl2.org/web/doxygen/lts__convert_8h_source

Retrieves the set of states from a `state_states_counter_example_index_triple`. This is a const member function.

```cpp
const set_of_states & states() const

```

--------------------------------

### run()

Source: https://mcrl2.org/web/doxygen/structmcrl2_1_1pbes__system_1_1absinthe__algorithm

Executes the main algorithm with a PBES and abstraction settings.

```APIDOC
## POST /websites/mcrl2_web/absinthe_algorithm/run

### Description
Runs the absinthe algorithm on a given PBES, with specified abstraction text and an over-approximation flag.

### Method
POST

### Endpoint
/websites/mcrl2_web/absinthe_algorithm/run

### Parameters
#### Request Body
- **_p_** (pbes&) - Required - The PBES object to process.
- **_abstraction_text_** (const std::string&) - Required - The text defining the abstraction.
- **_is_over_approximation_** (bool) - Required - Flag indicating if over-approximation should be used.
```

--------------------------------

### Get Initial State of the Game

Source: https://mcrl2.org/web/doxygen/pbes_2include_2mcrl2_2pbes_2rewriters_2enumerate__quantifiers__rewriter_8h_source

Returns the initial state of the parity game as a propositional variable instantiation. This represents the starting point for solving the game.

```cpp
virtual propositional_variable_instantiation get_initial_state()

```

--------------------------------

### Create Initial Partition (GJKW)

Source: https://mcrl2.org/web/doxygen/group__part__refine

Initializes the partition for the GJKW bisimulation algorithm. It takes boolean flags to control branching and divergence preservation.

```cpp
template<class LTS_TYPE >
void mcrl2::lts::detail::bisim_partitioner_gjkw< LTS_TYPE >::create_initial_partition_gjkw(bool _branching_, bool _preserve_divergence_)

```

--------------------------------

### Getting iterator to the first argument of an aterm

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1action__formulas_1_1forall

Provides a constant iterator pointing to the first argument of an aterm. This is the starting point for iterating through the arguments.

```cpp
const_iterator begin () const
```

--------------------------------

### Constructor

Source: https://mcrl2.org/web/doxygen/xinput__tool_8h_source

Initializes an xinput_tool with the specified name, author, description, and input file constraints.

```APIDOC
## mcrl2::utilities::tools::xinput_tool::xinput_tool

### Description
Constructor for the xinput_tool class.

### Method
Constructor

### Endpoint
N/A

### Parameters
- **name** (const std::string &) - The name of the tool.
- **author** (const std::string &) - The author of the tool.
- **what_is** (const std::string &) - A brief description of what the tool does.
- **tool_description** (const std::string &) - A detailed description of the tool's functionality.
- **known_issues** (std::string, optional) - A string detailing any known issues. Defaults to "".
- **min** (uint16_t, optional) - The minimum number of input files required. Defaults to 0.
- **max** (uint16_t, optional) - The maximum number of input files allowed. Defaults to 0 (no limit).

### Request Example
```cpp
xinput_tool my_tool("my_tool", "Me", "Does something", "This tool processes input files.", "", 1, 5);
```

### Response
N/A
```

--------------------------------

### Get Counter Example from BDD (C++)

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1data_1_1detail_1_1BDD__Prover

Returns all guards on a path leading to a 'false' leaf in the BDD, if such a path exists. This is an inline public method.

```cpp
inline
data_expression mcrl2::data::detail::BDD_Prover::get_counter_example()
```

--------------------------------

### C++: Get Stochastic Distribution from Initializer

Source: https://mcrl2.org/web/doxygen/stochastic__specification_8h_source

Retrieves the stochastic distribution associated with a stochastic process initializer. This distribution defines the probabilistic behavior of the process at its start.

```cpp
const stochastic_distribution & mcrl2::lps::stochastic_process_initializer::distribution() const
**Definition** stochastic_process_initializer.h:43
```

--------------------------------

### Initial Partition Creation in bisim_partitioner_gj_lazy_BLC

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1bisim__partitioner__gj__lazy__BLC

This function is responsible for setting up the initial state partitioning. It forms the basis for the subsequent refinement steps in the branching bisimulation algorithm.

```cpp
void | create_initial_partition ()
| create the initial partition for (branching) bisimulation
```

--------------------------------

### PBES Explorer Get Initial State (C++)

Source: https://mcrl2.org/web/doxygen/pbes_2include_2mcrl2_2pbes_2enumerator_8h_source

Returns the initial state of the PBES system. This is the starting point for any state-space exploration.

```cpp
ltsmin_state get_initial_state() const
Returns the initial state.
**Definition** pbes_explorer.cpp:1376
```

--------------------------------

### Transition Partitioning Utilities (C++)

Source: https://mcrl2.org/web/doxygen/lts__io_8h_source

Manages transition partitions for the bisim_dnj algorithm. Includes structures for predecessor and successor entries, and functions for manipulating transitions during partitioning, such as moving them between blocks or adapting them to non-inert states.

```C++
namespace mcrl2::lts::detail::bisim_dnj {

struct part_trans_t {
    // ... constructors and other methods ...

    // Array containing all predecessor entries.
    fixed_vector< pred_entry > pred;

    // Number of new bottom states found until now.
    state_type nr_of_new_bottom_states;

    // Pointer to the first inert transition in action_block.
    action_block_entry * action_block_inert_begin;

    // Number of nontrivial bunches.
    trans_type nr_of_nontrivial_bunches;

    // Array containing all block_bunch entries.
    fixed_vector< block_bunch_entry > block_bunch;

    // Pointer to the first inert transition in block_bunch.
    block_bunch_entry * block_bunch_inert_begin;

    // Destructor.
    ~part_trans_t();

    // Pointer to the first inert transition in the initial partition.
    const action_block_entry * action_block_orig_inert_begin;

    // Handle one transition after a block has been split, phase 2.
    void second_move_transition_to_new_action_block(pred_entry *const pred_iter);

    // Array containing all successor entries.
    fixed_vector< succ_entry > succ;

    // Adapt the non-inert transitions in an out-slice to a new block.
    succ_entry * move_out_slice_to_new_block(succ_entry *out_slice_end, ONLY_IF_DEBUG(const bisim_partitioner_dnj< LTS_TYPE > &partitioner,) block_t *const old_block, block_bunch_slice_const_iter_t const splitter_T);

    // Adapt data structures for a transition that has become non-inert.
    bool make_noninert(pred_entry *const old_pred_pos, block_bunch_slice_iter_or_null_t *const new_noninert_block_bunch_ptr);

    // Constructor.
    part_trans_t(trans_type num_transitions, trans_type num_actions);

    // Print all transitions.
    void print_trans(const bisim_partitioner_dnj< LTS_TYPE > &partitioner) const;

    // List of unstable block_bunch-slices.
    simple_list< block_bunch_slice_t > splitter_list;

    // Number of block_bunch_slices.
    trans_type nr_of_block_bunch_slices;

    // Transition is moved to a new bunch.
    void first_move_transition_to_new_bunch(action_block_entry *const action_block_iter, bunch_t *const bunch_T_a_Bprime, bool const first_transition_of_state);

private:
    // ... internal members ...
};

// ... other related classes and functions ...

}
```

--------------------------------

### Obtain Initial Distribution

Source: https://mcrl2.org/web/doxygen/data_2include_2mcrl2_2data_2find__equalities_8h_source

Retrieves the initial distribution for a given process identifier. This function is used to get the starting state distribution of a process in mCRL2.

```cpp
process_expression mcrl2::obtain_initial_distribution(const process_identifier &procId)
**Definition** linearise.cpp:9390
```

--------------------------------

### run

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1pbesinst__algorithm

Executes the PBES instantiation algorithm on a given PBES.

```APIDOC
## run()

### Description
Runs the PBES instantiation algorithm.

### Method
POST

### Endpoint
/pbesinst_algorithm/run

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **pbes** (pbes) - The PBES to process.

### Request Example
```json
{
  "pbes": { ... } 
}
```

### Response
#### Success Response (200)
- **status** (string) - Indicates that the algorithm has started or completed.

#### Response Example
```json
{
  "status": "Algorithm started successfully."
}
```
```

--------------------------------

### create_counter_example_lps()

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1lps__solve__structure__graph__algorithm

Creates a linear process specification that serves as a counter-example for a given PBES problem.

```APIDOC
## POST /create_counter_example_lps

### Description
Creates a linear process specification that serves as a counter-example for a given PBES problem.

### Method
POST

### Endpoint
/create_counter_example_lps

### Parameters
#### Request Body
- **G** (structure_graph&) - Required - The structure graph associated with the PBES.
- **V** (std::set<structure_graph::index_type>&) - Required - A set of indices representing vertices in the structure graph.
- **lpsspec** (lps::specification&) - Required - The original LPS specification.
- **p** (pbes&) - Required - The PBES to generate a counter-example for.
- **p_index** (pbes_equation_index&) - Required - The index of the PBES equation.

### Request Example
```json
{
  "G": "<structure_graph_data>",
  "V": [0, 1, 2],
  "lpsspec": "<lps_specification_data>",
  "p": "<pbes_data>",
  "p_index": "<pbes_equation_index_data>"
}
```

### Response
#### Success Response (200)
- **counter_example_lps** (lps::specification) - The generated LPS specification representing the counter-example.

#### Response Example
```json
{
  "counter_example_lps": "<lps_specification_data_for_counter_example>"
}
```
```

--------------------------------

### Get Maximum Function Name in C++

Source: https://mcrl2.org/web/doxygen/bool_8h_source

Retrieves the identifier string for the 'maximum' function. This is used to refer to the function symbolically, for example, in tool configurations or analysis.

```cpp
const core::identifier_string & maximum_name()
```

--------------------------------

### Get Iterator to Beginning of Tree

Source: https://mcrl2.org/web/doxygen/probabilistic__state_8h_source

Returns an iterator pointing to the first element of the term_balanced_tree. This is the starting point for iterating through the tree's contents.

```cpp
iterator begin() const
// Returns an iterator pointing to the beginning of the term_balanced_tree.
```

--------------------------------

### Constructor

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1pbesinst__algorithm

Initializes the PBES instantiation algorithm with a data specification, rewrite strategy, and an option to print equations.

```APIDOC
## pbesinst_algorithm()

### Description
Constructor for the PBES instantiation algorithm.

### Method
CONSTRUCTOR

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
```json
{
  "data_spec": "data_specification",
  "rewrite_strategy": "jitty",
  "print_equations": false
}
```

### Response
#### Success Response (200)
N/A (Constructor)

#### Response Example
N/A
```

--------------------------------

### Get Initial Distribution (Stochastic Specification)

Source: https://mcrl2.org/web/doxygen/namespacemcrl2_1_1lps

Retrieves the initial stochastic distribution from an lps::stochastic_specification. This provides access to the starting probability distribution of the model.

```cpp
const stochastic_distribution & | initial_distribution (const lps::stochastic_specification &lpsspec)
```

--------------------------------

### Counterexample Constructor

Source: https://mcrl2.org/web/doxygen/lts__convert_8h_source

The `counter_example_constructor` class is designed to store and manage counterexample trees. It provides methods to add transitions and save the constructed counterexample.

```cpp
class mcrl2::lts::detail::counter_example_constructor

```

```cpp
void save_counter_example(index_type index, const LTS_TYPE &l, const std::vector< size_t > &extra_actions=std::vector< size_t >()) const

```

```cpp
index_type add_transition(std::size_t label_index, index_type previous_entry)

```

--------------------------------

### PBES Instantiation Algorithms

Source: https://mcrl2.org/web/doxygen/structmcrl2_1_1pbes__system_1_1no__strategy

This section details various algorithms for instantiating PBES (Process Algebra Bisimulation Equation System), which is a crucial step in solving and analyzing these systems.

```APIDOC
## PBES Instantiation Algorithms

### Description
Provides various algorithms for instantiating PBES.

### Endpoints

- `pbesinst_algorithm`
- `pbesinst_alternative_lazy_algorithm`
- `pbesinst_finite_algorithm`
- `pbesinst_lazy_algorithm`
- `pbesinst_structure_graph_algorithm`
- `pbesinst_symbolic_algorithm`
- `pbesinst_rename`

### Usage Examples

```javascript
// Example of using a PBES instantiation algorithm
// const instantiated_pbes = mCRL2.pbesinst_algorithm(pbes_spec, parameters);

// Example of using the lazy instantiation algorithm
// const lazy_inst = mCRL2.pbesinst_lazy_algorithm(pbes_spec);
```
```

--------------------------------

### Get LPS Initial Process

Source: https://mcrl2.org/web/doxygen/balance__nesting__depth_8h_source

Returns a constant reference to the initial process expression of the LPS specification. This allows inspection of the starting state.

```C++
const InitialProcessExpression & mcrl2::lps::specification_base::initial_process() const
{
  // Accessor implementation details here
}
```

--------------------------------

### pbesinst_algorithm Constructor and Methods (C++)

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1pbes__system_1_1pbesinst__algorithm-members

This snippet details the constructor and key methods of the 'pbesinst_algorithm' class. The constructor initializes the algorithm with a data specification and an optional rewriter strategy and print flag. Methods like 'get_result' retrieve the algorithm's outcome, 'rewriter' provides access to the rewriter, and 'print_equations' handles the output of equations. These are fundamental for processing and instantiating PBES.

```cpp
pbesinst_algorithm(data::data_specification const &data_spec, data::rewriter::strategy rewrite_strategy=data::jitty, bool print_equations=false)
inline explicit pbesinst_algorithm(data::data_specification const &data_spec, data::rewriter::strategy rewrite_strategy=data::jitty, bool print_equations=false);

inline T get_result() const;

inline data::rewriter const& rewriter() const;

inline void print_equations() const;

inline void print_equation_count(std::size_t size) const;

```

--------------------------------

### Get Left-Hand Sides of Assignments in C++

Source: https://mcrl2.org/web/doxygen/mutable__map__substitution_8h_source

Extracts the left-hand side variables from a list of assignments. This function is useful when analyzing assignment statements, for example, to determine which variables are being modified.

```C++
variable_list left_hand_sides(const assignment_list &x)
// Returns the left hand sides of an assignment list.
**Definition** assignment.h:307
```

--------------------------------

### Counter Example Constructor

Source: https://mcrl2.org/web/doxygen/simple__list_8h_source

Documentation for the `counter_example_constructor` class used for storing counterexample trees.

```APIDOC
## Counter Example Constructor

### Description
A class designed to facilitate the construction and storage of counterexample trees, typically used in model checking to represent paths that violate certain properties.

### Class
- **`mcrl2::lts::detail::counter_example_constructor`**
- **Definition**: `liblts_bisim_gjkw.cpp:3052`
```

--------------------------------

### BLC_indicators_lb Status and Debugging

Source: https://mcrl2.org/web/doxygen/sim__hashtable_8h_source

Includes functions to check if transitions start in a small subblock, if the indicators represent a stable state, and to get a debug identifier.

```C++
bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::starts_in_small_subblock

```

```C++
bool mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::is_stable() const

```

```C++
std::string mcrl2::lts::detail::bisimulation_gj_lazy_BLC::BLC_indicators_lb::debug_id(const bisim_partitioner_gj_lazy_BLC< LTS_TYPE > &partitioner) const

```

--------------------------------

### Get Initial Stochastic Distribution

Source: https://mcrl2.org/web/doxygen/explorer__options_8h_source

Retrieves the initial stochastic distribution from a stochastic specification. This is crucial for analyzing the starting state of a probabilistic system.

```cpp
const stochastic_distribution & initial_distribution(const lps::stochastic_specification &lpsspec)
```

```cpp
const stochastic_distribution & initial_distribution(const lps::specification &)
```

--------------------------------

### Load LTS

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1counter__example__constructor-members

Loads a labeled transition system from a specified source.

```APIDOC
## POST /websites/mcrl2_web/load_lts

### Description
Loads a labeled transition system from a file or a string.

### Method
POST

### Endpoint
/websites/mcrl2_web/load_lts

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
- **source** (string) - Required. The source of the LTS data (e.g., file path or string).
- **format** (string) - Optional. The format of the LTS data if not auto-detectable.

### Request Example
```json
{
  "source": "path/to/your/lts.lts",
  "format": "lts"
}
```

### Response
#### Success Response (200)
- **status** (string) - Indicates the status of the loading operation.
- **lts_identifier** (string) - A unique identifier for the loaded LTS.

#### Response Example
```json
{
  "status": "success",
  "lts_identifier": "lts_12345"
}
```
```

--------------------------------

### Dummy Counter Example Get Trace Method (C++)

Source: https://mcrl2.org/web/doxygen/tree__set_8h_source

Returns an empty or default trace, as no actual trace is generated by the dummy implementation. This method is part of `dummy_counter_example_constructor`.

```cpp
trace get_trace(const LTS_TYPE &, index_type) const
```

--------------------------------

### create_counter_example_lps()

Source: https://mcrl2.org/web/doxygen/functions_c

Creates a counter example LPS structure graph algorithm.

```APIDOC
## create_counter_example_lps()

### Description
Creates a counter example LPS structure graph algorithm.

### Method
N/A

### Endpoint
N/A

### Parameters
N/A

### Request Example
N/A

### Response
N/A

### Response Example
N/A
```

--------------------------------

### Get Initial Vertex from Structure Graph Builder (C++)

Source: https://mcrl2.org/web/doxygen/structure__graph__builder_8h_source

Retrieves the index of the initial vertex in the structure graph. This provides access to the designated starting vertex.

```C++
structure_graph::index_type initial_vertex() const
```

--------------------------------

### lps2pbes Usage Example

Source: https://mcrl2.org/web/user_manual/tools/release/lps2pbes

Demonstrates the basic command-line usage of the lps2pbes tool. It requires a formula file and optionally takes input and output files for the linear process and the generated PBES.

```bash
lps2pbes   [OPTION]... --formula=FILE [INFILE [OUTFILE]]
```

--------------------------------

### MCRL2: Get Iterator to Start of Same BLC

Source: https://mcrl2.org/web/doxygen/liblts__weak__bisim_8h_source

The `start_same_BLC` member variable provides an iterator pointing to the beginning of a sequence of identical BLC indicators. This complements `end_same_BLC` for iterating over related BLCs.

```cpp
BLC_list_iterator mcrl2::lts::detail::bisimulation_gj::BLC_indicators::start_same_BLC;
```

--------------------------------

### Bisimulation Partitioner Initialization Helper

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1lts_1_1detail_1_1bisim__gjkw_1_1bisim__partitioner__gjkw__initialise__helper

Helper functions for initializing the bisim_gjkw bisimulation partitioner.

```APIDOC
## Bisimulation Partitioner Initialization Helper

### Description
Helper functions used during the initialization of the bisim_gjkw bisimulation partitioner.

### Methods

- **action_block_map**: Maps actions to blocks.
- **aut**: Accesses the automaton.
- **extra_kripke_states**: Manages extra Kripke states.
- **inert_in_per_state**: Handles inert incoming transitions per state.
- **inert_out_per_block**: Handles inert outgoing transitions per block.
- **inert_out_per_state**: Handles inert outgoing transitions per state.

### Endpoint
N/A (Internal library functions)

### Parameters
N/A (These are static methods or members of a helper class)

### Request Body
N/A

### Response
N/A (Return types vary depending on the method)

### Examples
N/A (Usage within the mcrl2 library codebase)
```

--------------------------------

### Get Iterator to Beginning of Balanced Tree (C++)

Source: https://mcrl2.org/web/doxygen/liblts__coupledsim_8h_source

Returns an iterator pointing to the beginning of the term_balanced_tree. This method is essential for iterating over the elements of the tree from the start. It returns a constant iterator.

```cpp
iterator begin() const
{
    // Implementation details would go here
    return iterator();
}
```

--------------------------------

### Initialize and Use execution_timer

Source: https://mcrl2.org/web/doxygen/classmcrl2_1_1utilities_1_1execution__timer

Demonstrates the basic usage of the execution_timer class by initializing it with a tool name and filename, starting a timed section, executing code, finishing the timed section, and generating a report.

```cpp
execution_timer timer("test_tool", "/path/to/file");
timer.start("hint");
// ... (execute some code here) ...
timer.finish("hint");
timer.report();
```

--------------------------------

### Get Counter Example from BDD in C++

Source: https://mcrl2.org/web/doxygen/bdd__prover_8h_source

Retrieves the guards from a path within the BDD that leads to a 'false' leaf node. This represents a counter-example.

```cpp
data_expression get_counter_example()
```
Tokens:
Raw