Documentation ¶
Index ¶
- Constants
- func CheckEvents(model Model, history []Event) bool
- func CheckOperations(model Model, history []Operation) bool
- func DefaultDescribeOperation(input interface{}, output interface{}) string
- func DefaultDescribeState(state interface{}) string
- func NoPartition(history []Operation) [][]Operation
- func NoPartitionEvent(history []Event) [][]Event
- func ShallowEqual(state1, state2 interface{}) bool
- func Visualize(model Model, info linearizationInfo, output io.Writer) error
- func VisualizePath(model Model, info linearizationInfo, path string) error
- type CheckResult
- func CheckEventsTimeout(model Model, history []Event, timeout time.Duration) CheckResult
- func CheckEventsVerbose(model Model, history []Event, timeout time.Duration) (CheckResult, linearizationInfo)
- func CheckOperationsTimeout(model Model, history []Operation, timeout time.Duration) CheckResult
- func CheckOperationsVerbose(model Model, history []Operation, timeout time.Duration) (CheckResult, linearizationInfo)
- type Event
- type EventKind
- type Model
- type Operation
Constants ¶
View Source
const ( Unknown CheckResult = "Unknown" // timed out Ok = "Ok" Illegal = "Illegal" )
Variables ¶
This section is empty.
Functions ¶
func CheckEvents ¶
func CheckOperations ¶
func DefaultDescribeOperation ¶
func DefaultDescribeOperation(input interface{}, output interface{}) string
func DefaultDescribeState ¶
func DefaultDescribeState(state interface{}) string
func NoPartition ¶
func NoPartitionEvent ¶
func ShallowEqual ¶
func ShallowEqual(state1, state2 interface{}) bool
func VisualizePath ¶
Types ¶
type CheckResult ¶
type CheckResult string
func CheckEventsTimeout ¶
func CheckEventsTimeout(model Model, history []Event, timeout time.Duration) CheckResult
timeout = 0 means no timeout if this operation times out, then a false positive is possible
func CheckEventsVerbose ¶
func CheckEventsVerbose(model Model, history []Event, timeout time.Duration) (CheckResult, linearizationInfo)
timeout = 0 means no timeout if this operation times out, then a false positive is possible
func CheckOperationsTimeout ¶
func CheckOperationsTimeout(model Model, history []Operation, timeout time.Duration) CheckResult
timeout = 0 means no timeout if this operation times out, then a false positive is possible
func CheckOperationsVerbose ¶
func CheckOperationsVerbose(model Model, history []Operation, timeout time.Duration) (CheckResult, linearizationInfo)
timeout = 0 means no timeout if this operation times out, then a false positive is possible
type Model ¶
type Model struct { // Partition functions, such that a history is linearizable if an only // if each partition is linearizable. If you don't want to implement // this, you can always use the `NoPartition` functions implemented // below. Partition func(history []Operation) [][]Operation PartitionEvent func(history []Event) [][]Event // Initial state of the system. Init func() interface{} // Step function for the system. Returns whether or not the system // could take this step with the given inputs and outputs and also // returns the new state. This should not mutate the existing state. Step func(state interface{}, input interface{}, output interface{}) (bool, interface{}) // Equality on states. If you are using a simple data type for states, // you can use the `ShallowEqual` function implemented below. Equal func(state1, state2 interface{}) bool // For visualization, describe an operation as a string. // For example, "Get('x') -> 'y'". DescribeOperation func(input interface{}, output interface{}) string // For visualization purposes, describe a state as a string. // For example, "{'x' -> 'y', 'z' -> 'w'}" DescribeState func(state interface{}) string }
Click to show internal directories.
Click to hide internal directories.