For internal use only.

Returns the unmodifiable (read-only) set of states that follow this state if we transition along an event. @param event @return

Given a set of invariants, a new set containing only constrained IntrBy invariants @param invariants The original set of invariants @retur

Returns a regular expression for a tail with the given tail events and follow set.

Gets an element of a repeated field. For primitive fields, the boxed primitive value is returned. For enum fields, the EnumValueDescriptor for the v

Gets the number of elements of a repeated field. This is exactly equivalent to calling the generated "Count" accessor method corresponding to the fie

Returns ResultSet of "SELECT from ReExp" query. Note: must call close() on ResultSet after done using it. @param field @param value @return ResultSet

Get the FieldAccessorTable for this type. We can't have the message class pass this in to the constructor because of bootstrapping trouble with Descr

Whether or not the FSM state is a valid terminal state for the FSM.

@return Whether or not this is a unit vector

Create a new {@code CodedOutputStream} wrapping the given {@code OutputStream}.

Returns the event at the top of the queue, without removing it.

Recomputes the alphabet of the FSM based on current states.

Retrieves session state and sets/reconstructs the local variables.

Runs invarimint with given command line args and returns the derived EncodedAutomaton model. @param args @return @throws Exception

Constructs a Graphviz dot representation of the model.

* Returns the point that is the weighted sum of the specified control points, * using the specified weights. This method requires that there are fo

Adds a symbol to the symbol table. If a symbol with the same name already exists, throws an error.

Check that the type/pre- and post-event states of each log event in the list is correct. @throws ParseException

Clears the display state of the edges, i.e. sets them all back to default.

Clears the field. This is exactly equivalent to calling the generated "clear" accessor method corresponding to the field.

Helper method for compareTo(). Returns -2 if both objects are non-null. Otherwise, returns 1, 0, or -1 if respectively just o1 is null, both are null,

Compute the number of bytes that would be needed to encode a {@code bytes} field, including tag.

Delta computation, incrementing, and division are undefined for vector timestamps.

Compute the number of bytes that would be needed to encode an {@code int64} field, including tag.

@return mean delta resource for transition, null if transition has zero delta resources.

@return mode delta resource for transition, null if transition has zero delta resources.

A stricter equality check against another GFSM. This is equality check is for states and the transitions, but not any observed states. Two GFSMs are e

Determines and returns the ith event for node identified by nodeIndex in a sequence of events. Precondition: nodeIndex must be valid.

Draws PO invariants within a column on paper and links the generated invariants to their corresponding grid labels. @param invs @param col @param gwt

Set the end of the violation subpath to this node. This node's label should always be the invariant's second predicate.

Exports the CFSM to a format determined by GraphExportFormatter, writing the resulting string to a file specified by fileName. Each FSM in CFSM is exp

Common code for testing failure states of tracing sets for constrained invariants

Create partition graph from passed log of events, then generate and return the map of each partition to its final constrained tracing state sets, wher

Parsers events using the supplied parser, generates the initial _partitioning_ graph and returns it to the caller. @param miner @throws Exception

@return y value of the path's bounding box

Returns an EventTypeEncodings object for event {a, b, c, d}.

Returns Daikon invariants associated with the transition, or null if none exist.

Get an empty {@code UnknownFieldSet}.

Returns the set of partitions that are initial for a pid.

Return the singleton instance of SynopticMain, first asserting that the instance isn't null.

Returns the set of ITemporalInvariants composing this model.

Returns the value for a particular label type. If none exist, then returns null.

This call returns the tab's Panel widget that holds the tab's contents.

Event name in Promela. This prevents the use of a Promela keyword as an event type.