Get the proto package name. This is the package name given by the {@code package} statement in the {@code .proto} file, which differs from the Java p

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

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

Sets a field to the given value. The value must be of the correct type for this field, i.e. the same type that {@link Message#getField(Descriptors.Fi

Set the time when this event occurred @param t the time

Splits the partitions in {@code pGraph} until ALL synoptic.invariants returned by {@code pGraph.getInvariants()} are satisfied. @param pGraph

Stop the timed task. This takes the current system time and saves it. Calling stop on TimedTasks that have been stopped before has no effect. If the t

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

Removes and returns the event at the top of the queue.

Generates an initial graph using the supplied parser. @param events log of events @return an initial graph corresponding to the log of eve

Constructs a CFSM from a GFSM. It performs the necessary traversal of the GFSM to construct/specify all the process FSMs that should be part of the CF

If this is a nested type, get the outer descriptor, otherwise null.

The set of possible (abstract, non-observed) event types that can trigger a transition from this state.

Returns true if the given field is set. This is exactly equivalent to calling the generated "has" accessor method corresponding to the field. @throws

Get the message being built. We don't just pass this to the constructor because it becomes null when build() is called.

Create a new {@link Builder}.

Sets the style of the displayed edge <p> IMPORTANT NOTE: When changing the state of the edges in the Dracula Model make sure to change the attributes

Generates a Promela representation of this CFSM, to be used with SPIN. The never claim is not specified here and it is appended to the CFSM elsewhere.

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

Encode and write a varint. {@code value} is treated as unsigned, so it won't be sign-extended if negative.

Adds a transition on e from this to s.

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

Compute the number of bytes that would be needed to encode a varint. {@code value} is treated as unsigned, so it won't be sign-extended if negative.

Exports this Builder's model as a Graphviz dot file and associated png. Limits the alphabet of this model to currently encoded characters, such that n

Generates an initial graph using the supplied parser. @param events log of events @return an initial graph corresponding to the log of eve

Converts a dot file as a png image file using dot. The png file will be created in the same place as the dot file. @param dotFile dot file

Get a field builder for the given field number which includes any values that already exist.

Returns the set of all observations mapped to this partition.

Intersects this InvsModel with all of the given InvModels and adds each to this model's list of invariants.

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

Sets the partitioning filter, to the passed, back-reference containing string.

Converts an array of strings into a list of EventType objects. Does not handle INITIAL or TERMINAL events types.

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

Augments the CFSM with synthetic events for model checking binv. <p> The basic strategy, regardless of invariant, is to create a separate FIFO queue t

Checks that the type/time of each log event in a list is correct. @param events List of occurrences to check @param timeStrs Ar

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

Creates and returns a JSGraph instance.

Tests for trace graph equality.

Returns a list of paths, each of which violates an invariant maintained by this invariant set (i.e. each of which is a counter-example). @param <T>

Get the short name of the invariant (e.g. "AP" for "AlwaysPrecedes) @return a short invariant name string

Retrieve the set of messages marked so far. @return the set of marked nodes

Returns this state's id.

Returns the time series associated with the transition, or null if none exist.