Merge partitions in pGraph that are k-equal (kTails equality), with k=0 without unsatisfying any of the pGraph invariants.. @param pGraph

Returns a {@link ParseException} with the current line and column numbers in the description, suitable for throwing.

Runs the model checker on the input string representation of the CFSM. Times out the process after timeoutSecs.

Verifies that the field is a field of this message.

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

Mark an event for splitting into a separate node. @param event the event to mark

Creates a set of nodes based on the labels array. Adds these nodes to the graph, but does not create any transitions between them. Returns the set of

Helper for DynamicMessage.parseFrom() methods to call. Throws {@link InvalidProtocolBufferException} instead of {@link UninitializedMessageException}

Change the state of the process.

Draws the graph. Must be called after the nodes and edges have all been added.

@return true if the language of this FSM is equal to the language of the given FSM.

Export g as a non-initial graph.

Called by subclasses to check if all extensions are initialized.

Generates an initial linear graph based on a sequence of log events. Uses the defParser parser for parsing the log of events. @param events

Returns this model's invariant.

Given an array of strings, create a list of corresponding LogEvent instances. @param strEvents A string sequence of events. @return A LogE

Get the field's number.

Returns the probability associated with this transition. If none is associated, returns null.

Get all relations that appear in this graph. @return the set of relations in the graph

@return true if this FSM is deterministic.

Updates the local time and logs a timestamped event.

Makes a tag value given a field number and wire type.

Construct a {@link Message.Builder} for the given type.

Creates a new DistEventType that is an INITIAL.

Read a {@code bytes} field value from the stream.

Read an enum field value from the stream. Caller is responsible for converting the numeric value to an actual enum.

Read an {@code int64} field value from the stream.

Converts this chain into a RelationPath list.

Converts a list of DistEventType instances into a set, and returns the set.

Creates a set of nodes based on the labels array. Adds these nodes to the graph, but does not create any transitions between them. Returns the set of

Adds a single event node to the current partition. @param eNode event node to add

Builds a generic string to describe a location of an error on a line in some input file.

Checks that state contains the expected variables and values.

Implements a heuristic for choosing a subset of the invariants that we want to check. The basic idea is that there may be events that are associated w

VectorTime is only partially ordered, therefore compareTo cannot be used to derive a total ordering of a set of VectorTime instances. Instead, compare

@return Maximum resource delta for transition, or null if transition has no resource deltas

@return Minimum resource delta for transition, or null if transition has no resource deltas

Copies the given bytes into a {@code ByteString}.

Create a new task. @param string the task name. Choose something unique. @return the timed task created

Exports the graph to a format determined by Main.graphExportFormatter, writing the resulting string to a file specified by fileName.

Called by subclasses to compute the size of extensions.

Generate a partition graph with constrained invariants using the passed log of events with integer timestamps, e.g., {"a 1", "b 4"} @param events

Returns the accept states for the FSM.

Returns the count associated with this transition. If none is associated, returns null.

Get a list of this message type's fields.

Returns the initial states for the FSM.