All Classes and Interfaces
Class
Description
Contains 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.
Utility class for exception handling.
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.
Utility class for file operations related to storing and reading task schedules.
Exception thrown to halt execution of the current and all subsequent executions.
Exception thrown to halt execution of the current execution.
Error type when the model checker stops the execution.
Exception thrown to halt execution of the current task.
The JmcAssume class provides a method to assert conditions in the JMC runtime environment.
A redefinition of
AtomicBoolean that communicates with JMC
runtime to perform read, write, and compare-and-set operations.A redefinition of
AtomicInteger for JMC model checking.A redefinition of
AtomicReference to support JMC model
checking.A redefinition of the
AtomicReferenceArray class.A mandatory annotation to mark a test method or class to be run with the JMC model checker.
Configuration annotation for JMC checks.
Configuration for the JMC checker.
Builder for JmcCheckerConfiguration
Exception class for JMC checker errors.
Exception class for JMC checker timeout errors.
A JUnit 5 test descriptor for a JMC class test.
A JMC-specific version of
CompletableFuture that allows for custom
execution and provides a way to set an underlying JmcFuture.Utility class for handling JMC descriptor configurations.
A JUnit 5 engine descriptor for the JMC engine.
A JMC executable test descriptor for JUnit 5.
A replacement for
Executors.An executor service that runs tasks in new threads.
This annotation is used to mark a test method or class to expect an assertion failure in the JMC
model checker.
This annotation is used to mark a test method or class to expect a certain number of executions
in the JMC model checker.
A functional test target for JMC that allows invoking a target method.
Represents a target for JMC.
A future that runs a callable function in a new thread.
This annotation is used to mark methods or classes that should be ignored by the JMC instrumentation.
Exception class for JMC invalid configuration errors.
Exception thrown when an invalid strategy is encountered.
The LockSupport class is the replacement for
LockSupport
class.This annotation is used to configure the JMC graph coverage measurement for a test method or
class.
A JUnit 5 test descriptor for a JMC method test.
The JmcModelChecker class is responsible for managing the model checking process.
The JmcModelCheckerReport class represents a report generated by the JMC model checker.
A JMC-specific implementation of java.util.Random that allows for model checking.
A reentrant lock that can be used to synchronize access to shared resources.
This annotation is used to mark a test method or class to be replayed in the JMC model checker.
Exception thrown when replay is not supported by the current strategy.
The Runtime environment complete with a scheduler and configuration options used by the model
checker.
Represents the configuration for the JMC runtime.
Represents an event that occurs during the execution of a program.
A builder for constructing a
JmcRuntimeEvent object.Enum representing the different types of runtime events that can occur.
Utility class for JMC runtime operations.
A custom JUnit 5 test engine for running JMC tests.
Executes a JMC test method using the JMC Model Checker.
Represents a target for JMC.
This class is a wrapper around the Java Thread class -
Thread.A thread factory that creates
JmcThread instances.A thread pool executor that runs tasks in new threads.
This annotation is used to specify a timeout for a test method or class when using the JMC model
checker.
This annotation is used to configure the JMC trust strategy for a test method or class.
Represents a Lamport vector clock used by the algorithm.
Represents a component of the Lamport vector clock.
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 generic partial order relation.
Represents the relation between two objects.
Represents a primitive value that is returned by a strategy.
Represents a primitive (Number|String|Boolean) value used in scheduling choices.
A random scheduling strategy that selects the next thread to be scheduled randomly.
A ReplayableSchedulingStrategy is a scheduling strategy that can record and replay its execution
trace.
The scheduler is responsible for managing the execution of threads.
Represents a scheduling choice in the JMC runtime.
A value that the strategy uses to communicate with the runtime yields.
An adapter to convert a JSON object to a
SchedulingChoiceValue.A factory for creating instances of
SchedulingChoiceValue.Represents a scheduling choice with an optional location.
The scheduling strategy is responsible for deciding which thread to schedule next.
Configuration class for scheduling strategies.
Factory class for creating scheduling strategies.
Utility class for string operations.
Exception thrown when a task is already paused.
Encapsulates all the operations related to Task objects used by the runtime Except the
SchedulerTask The encapsulation ensures no memory leak when creating many tasks.
The state of each task managed by the @RuntimeEnvironment is represented by one of the
following.
Exception thrown when a task does not exist.
Represents a generic total order relation.
Represents an exception thrown when an invalid comparison is attempted.
Represents the relation between two objects.
A strategy that tracks the active tasks.
Tracks the active tasks based on events.
Tracks the locks acquired and released events of tasks.
Tracks the tasks start finish and join request events.
A wrapper around the
Algo algorithm that implements a scheduling strategy based on trust.