Represents a single process that generates and consumes messages.

Receiver in an alternating bit protocol.

Sender in an alternating bit protocol.

Represents a set of ACWith invariants, closed under transitive closure. That is, if a and b are in the set, and b ACWith c, then c is also in the set.

Represents a birelational event invariant in the input traces where the first event is always followed by the second event.

FSM for a set of invariants of the form "A always followed by B". The FSM enters a failure state when A is encountered, and then enters a success stat

NFA state set for the AFbyLower constrained invariant which keeps the shortest path justifying a given state being inhabited. <br /> <br /> State0 = s

Represents a "A always followed by B" synoptic.invariants to simulate, recording the shortest historical path to reach a particular state. This finite

NFA state set for the AFbyUpper constrained invariant which keeps the shortest path justifying a given state being inhabited. <br /> <br /> State0 = s

Represents a birelational event invariant in the input traces where the first event is always preceded by the second event.

FSM for a set of invariants of the form "A always precedes B". The FSM enters a permanent success state upon encountering an A, and enters a permanent

NFA state set for the APLower constrained invariant which keeps the shortest path justifying a given state being inhabited. <br /> <br /> State0 = sta

Represents a set of "A always precedes B" synoptic.invariants to simulate, recording the shortest historical path to reach a particular state. This fi

NFA state set for the APUpper constrained invariant which keeps the shortest path justifying a given state being inhabited. <br /> <br /> State0 = sta

Describes a basic interface for an FSM.

An abstraction for a state of an FSM. This state can be initial/terminal, and has some number of transitions to other state instances. @param <NextSt

Implements basic functionality and maintains channel states for a number of processes in a FIFO system.

Partial specification for the non-channel state of multiple FSM processes. @param <State> The state of a single FSM process.

A callback object, which takes care of starting/stopping the associated progress wheel animation, and controlling the error message display. This clas

Contains entry points for the command line version of Synoptic or a derivative project. The AbstractMain instance is a singleton that maintains option

A partial implementation of the {@link Message} interface which implements as many methods of that interface as possible in terms of other methods. @

A partial implementation of the {@link MessageLite} interface which implements as many methods of that interface as possible in terms of other methods

<p> The common options for all Synoptic projects. Generally, this should not be created manually. Instead, parse command line options using PerfumeOpt

An interface that all Synoptic resource types must implement. It abstracts away the type of resource used -- vector clocks/integer/float/etc -- and ex

AbstractTestCase is a sequence of actions corresponding to a valid path in some Synoptic model.

Action is a single step in an abstract test case. Action is an INode that can have at most 1 outgoing transition.

Adds a new reg exp text area with a corresponding delete button.

This class keeps a set of transitive closures for an IGraph, one transitive closure per relation in the IGraph.

Exception thrown when a one-time callback is called more than once.

Represents the "x is always concurrent with y" invariant for some two distributed event types x and y. What this means is that for all the inputs trac

A CSight representation of the AFby invariant.

A CSight representation of the AP invariant.

Exposes an interface for GWT events to be tracked via Google analytics. All of the exposed methods are static JSNI methods. The client is required to

Singleton class that takes care of loading in all of the application configuration parameters. Currently, these are passed to the application as syste

Tests the server-side configuration object.

Tests the server-side configuration object.

Java wrapper for an arrow on a Raphael canvas

Represents a bad configuration in the CFSM, which will be tested for reachability by the McScM model checker. A bad configuration includes (1) a CFSM

A class to facilitate synoptic.benchmarks. Just set your benchmark up as a ConfigureableBenchmark, and pass it to the constructor. The synoptic.benchm

BiRelationalInvariants are invariants mined from subsets of input traces. The mined subset of an input trace is the set subtraces over relation, trans

Factory of binary invariant checkers, as well as the base class for all of these checkers.

Evaluates two objects and always returns false.

Class for code that is shared by all binary temporal synoptic.invariants.

A CSight representation a binary temporal invariant, inv(first,second), where first/second are the related event types. An invariant also includes syn

Evaluates two objects and always returns true.

Partition graphs can be transformed using two algorithms -- coarsening and refinement. This class implements refinement using the Bisim algorithm ( {@

<p>Abstract interface for a blocking RPC channel. {@code BlockingRpcChannel} is the blocking equivalent to {@link RpcChannel}. @author kenton@google

Blocking equivalent to {@link Service}. @author kenton@google.com Kenton Varda @author cpovirk@google.com Chris Povirk

The default brief log formatter used by Synoptic for logging to stdout.

Builder for {@link DynamicMessage}s.

A partial implementation of the {@link Message.Builder} interface which implements as many methods of that interface as possible in terms of other met

A partial implementation of the {@link Message.Builder} interface which implements as many methods of that interface as possible in terms of other met

Builder for {@link UnknownFieldSet}s. <p>Note that this class maintains {@link Field.Builder}s for all fields in the set. Thus, adding one element t

Used to build a {@link Field} within an {@link UnknownFieldSet}. <p>Use {@link Field#newBuilder()} to construct a {@code Builder}.