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

Used by CSight.<br/> <br/> Interprets/parses the String eType into either a local, a send, or a receive event. Can only be called once. For send/recei

Returns true if all partitions of the GFSM contain only one observed fifo state

Used to compare two resource values. Note that (x < y) || (y < x) is only true for totally ordered resource instances. It is not necessarily true for

Parse a text-format message from {@code input} and merge the contents into {@code builder}.

Creates a new DistEventType that is an TERMINAL.

Parses the channelSpec command line option value and returns a list of corresponding channelId instances. @throws Exception

Rounds off edge probability to two decimal places. Used by all edge formatters. NOTE: if this method is modified, make sure to update the synopticgwt.

@private Proxy the given property on the layer.

Sets the synthetic tracing event corresponding to first.

Associates an arbitrary label of type t with the transition. @param t The type of label. @param label An object representing th

Sets the options based on args array. Uses plume-lib for options processing and assumes that the plume options are defined as part of _this_ class ins

See {@link FileDescriptor#setProto}.

Sets the synthetic tracing event corresponding to second.

Returns an RE encoding an occurrence of any number of the synthetic events, in arbitrary order.

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

Increments vtime at an index and returns the new vtime @param index @return the newly created, incremented vtime

Test that the list of events representing a linear graph generates or not (depending on value of cExampleExists) a single counter-example for invarian

The list of partially ordered events is condensed into a partition graph (the most compressed model). This graph is then checked for existence or not

If the next token exactly matches {@code token}, consume it and return {@code true}. Otherwise, return {@code false} without doing anything.

Write a {@code bytes} field, including tag, to the stream.

Write an {@code int64} field, including tag, to the stream.

@private

Converts a partition graph into a GWTGraph @param partGraph partition graph @return Equivalent GWTGraph

Adds a collection of event nodes to the existing partition. Updates the partition's isTerminal flag. @param eNodes event nodes to add

Adds a delta to the series. If the series of deltas is missing, then one will be created. Cannot be called after a single delta has been successfully

Sets the event and the state (local to the same process) that followed this state.

Implements the (model check - refine loop). Check each invariant in dynInvs in the pGraph model, and refine pGraph as needed until all invariants are

Used to compare two resource values. Note that (x < y) || (y < x) is only true for totally ordered resource instances. It is not necessarily true for

Uses the miner passed into the constructor to first mine unconstrained invariants. Then walks the trace to compute constraints for AlwaysFollowedInvar

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

TODO: Needs testing. <br/> <br/> Computes a valid (one of many possible ones) topological ordering of vertices in the trace corresponding to traceid.

Returns the _initial_ consistent anonymous state for a process.

Assumes tracegraph is already constructed. Walks over the tracegraph that eNode is part of to populate seen, eventcounts, followedByCounts, precedesCo

Assumes tracegraph is already constructed. Walks over the tracegraph that eNode is part of to populate seen, eventcounts, followedByCounts, and preced

Interpret a character as a digit (in any base up to 36) and return the numeric value. This is like {@code Character.digit()} but we don't accept non-

Get an immutable empty FieldSet.

Serializes g using a dot/gml format and optionally outputs a png file corresponding to the serialized format (dot format export only). @param outputP

Exports the GFSM model, as well as the corresponding CFSM, and CFSM augmented with the invariant we are currently checking. @param pGraph @param curI

Constructs a parser used by tests concerning an integer time. Note: the parser may not be re-used for parsing different traces (it is stateful).

Returns the global performance metrics object

@return height of path's bounding box

Get a {@code DynamicMessage} representing the default instance of the given type.

Returns the event type of this partition.

Get the index of this descriptor within its parent. In other words, given a {@link FileDescriptor} {@code file}, the following is true: <pre> for a

Returns singleton instance of DerbyDB. @param path path of database @param isCreate whether or not to create new tables @return

Returns the filename for an intermediate dot file based on the given stage name and round number. Adheres to the convention specified above in usage,

Returns all the invariant pairs of a particular invariant type @param invType invariant type @return

Looks up the next state on an ABSTRACT dist event type.

Gets the partition that will be split. @return the partition that will be split

Returns paths through a set of partition nodes in the form of a map. The returned map maps a traceID to a path (list of partitions) that passes throug