stamina Namespace Reference

Classes
class	Stamina

Typedefs
typedef core::StaminaMessages	StaminaMessages

Detailed Description

A copy of storm::builder::ExplicitModelBuilder with a max number of states to explore for debugging purposes

The model builder class which implements the STAMINA 2.5 algorithm (STAMINA 2.0/2.1 with dynamic programming)

Created by Josh Jeppson on Jun 9, 2021

Implementation for StaminaModelBuilder methods.

Created by Josh Jeppson on 8/17/2021

The model builder class which implements the STAMINA 3.0 algorithm which uses a priority queue on the estimated reachability

Created by Josh Jeppson on Jun 9, 2021

The model builder class which implements the STAMINA 2.0 algorithm (no dynamic programming)

NOTE: This algorithm is here for testing purposes and benchmarking. It is NOT recommended to use this method

Created by Josh Jeppson on Jun 9, 2021

There are some benefits if only using one thread to using just the StaminaModelBuilder class or StaminaIterativeModelBuilder class. This class is used if and only if the threadcount is greater than 1.

Simply including threading makes it so that there is some nontrivial overhead in exploration, and we want to provide the users the option without having them have to have a control thread idling and waiting for the exploration thread.

Created by Josh Jeppson on Jul 15, 2022

There are some benefits if only using one thread to using just the StaminaModelBuilder class or StaminaPriorityModelBuilder class. This class is used if and only if the threadcount is greater than 1.

Simply including threading makes it so that there is some nontrivial overhead in exploration, and we want to provide the users the option without having them have to have a control thread idling and waiting for the exploration thread.

Created by Josh Jeppson on Jul 15, 2022

Base class for all types of threads used by Stamina's model builders

Created by Josh Jeppson on Jul 8, 2022

A type of thread which maintains the following responsibilities:

1. Keeps track of which thread owns a particular state
2. Allows for asynchronous requests for ownership of new states
3. Allows for unordered and asynchronous requests for transition matrix insertion

Created by Josh Jeppson on Jul 8, 2022

Exploration threads can explore a state space with other threads, and will only explore threads that it owns.

Created by Josh Jeppson on Jul 8, 2022

An implementation of the ExplorationThread abstract class which uses the STAMINA iterative (2.0/2.5) algorithm.

Created by Josh Jeppson

Method implementations for Stamina

Created on 8/17/2021 by Josh Jeppson

Because state indecies are generally assigned in order, it is more efficient to allocate a linear array which guarantees a O(1) lookup time and has an (at worst) O(n / blockSize) insert.

Blocksizes are assumed to be large

Implementation for StaminaMemoryPool methods

This file created by Josh Jeppson on May 27, 2022

Stamina Memory Pool allocator

Because STAMINA/STORM allocates thousands or millions of states, and in C++ each call to new invokes a system-call, dynamic allocation of memory for stamina::StaminaModelBuilder::ProbabilityStates are very slow. This allocates a pool of larger blocks to reduce the number of system-calls (since each call to malloc() – invoked by new – is a system call to ask for more memory)

This memory pool makes a few assumptions to increase performance:

1. All states are assumed to be in memory from allocation-time until the program. The STAMINA memory pool allows for dynamic deletion, but defragmentation must be explicitly invoked using the defrag() method and is not automatically called.
2. For now, defrag() has not been implemented, requiring

Future work:

1. Offload excess memory to a swapfile which is deleted on StateMemoryPool destruction

This file created by Josh Jeppson on May 27, 2022