Package org.mpi_sws.jmc.strategies.trust
package org.mpi_sws.jmc.strategies.trust
Defines the strategy for complete exhaustive model checking of the input program.
Based on the Paper "Truly stateless optimal dynamic partial order reduction" by Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis
-
ClassDescriptionContains the core Trust algorithm implementation.Represents a restricted view of the execution graph.Represents an event object used by the algorithm.A generic event predicate.Unique key for the event.Represents the type of the event according to the algorithm.Represents an execution graph.Generic visitor interface for the execution graph nodes.Topological sorter for the execution graph.Exception thrown when the graph has cycles.Represents a node in the execution graph.The exploration stack used in the Trust algorithm.Represents an item in the exploration stack.Represents the item type in the exploration stack.A single class to store references to locations and to keep track of location aliases.A scheduling strategy that measures the coverage of execution graphs during the model checking process.Configuration class for the MeasureGraphCoverageStrategy.Exception thrown when an event does not exist.Represents a scheduling choice with an optional location.A wrapper around the
Algoalgorithm that implements a scheduling strategy based on trust.