csp

package module
v0.1.1 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: May 6, 2024 License: AGPL-3.0 Imports: 3 Imported by: 0

Documentation

Overview

Package csp contains definitions of CSP processes and events.

Index

Constants

View Source 
const (
	// PrecedenceLeaf is the precedence of leaf processes: Stop, Skip, Ω, and
	// prefix.
	PrecedenceLeaf = Precedence(iota)
	PrecedenceSequentialComposition
	PrecedenceExternalChoice
	PrecedenceInternalChoice
	PrecedenceRecursion
	PrecedenceParallel
	PrecedenceHide
)

Variables

View Source 
var Tau tau

Tau is the builtin τ event.

View Source 
var Tick tick

Tick is the builtin ✔ event.

Functions

func ProcessHasTrace 

func ProcessHasTrace(p Process, t Trace) error

ProcessHasTrace returns whether a process can perform the events in a particular trace. If it cannot, we return a counterexample error: the prefix of the trace that the process _could_ perform, and the event that the process could not perform at that point.

Types

type Event 

type Event interface {
	// AsSet returns an [EventSet] containing only this event.
	AsSet() EventSet
}

Event is an event that a CSP process can perform.

type EventSet 

type EventSet struct {
	User UserEventSet
	// contains filtered or unexported fields
}

EventSet is a set of events.

func EmptyEventSet 

func EmptyEventSet() EventSet

EmptyEventSet returns an empty EventSet.

func Events 

func Events(user UserEventSet) EventSet

Events returns an EventSet that only contains the events in a UserEventSet.

func FromAnfSet 

func FromAnfSet(set anf.Set) EventSet

FromAnfSet translates an anf.Set into a set of CSP events.

func Intersection 

func Intersection(sets ...EventSet) EventSet

Intersection returns the intersection of zero or more event sets.

func Union 

func Union(sets ...EventSet) EventSet

Union returns the union of zero or more event sets.

func (*EventSet) Add 

func (es *EventSet) Add(other EventSet)

Add adds the events in another event set to this one.

func (EventSet) Contains 

func (es EventSet) Contains(event any) bool

Contains returns whether an event set contains a particular event.

func (EventSet) Difference 

func (es EventSet) Difference(other EventSet) EventSet

Difference returns an event set that includes events that are in this event set but not in `other`.

func (EventSet) Equal 

func (es EventSet) Equal(other EventSet) bool

Equal returns whether two event sets contain exactly the same set of events.

func (EventSet) Format 

func (es EventSet) Format(f fmt.State, verb rune)

func (EventSet) HasNonemptyIntersection 

func (es EventSet) HasNonemptyIntersection(other EventSet) bool

HasNonemptyIntersection returns whether there are any events that are both in this event set and another.

func (*EventSet) Intersect 

func (es *EventSet) Intersect(other EventSet)

Intersection removes events from this event set that aren't also in another.

func (EventSet) Intersection 

func (es EventSet) Intersection(other EventSet) EventSet

Intersection returns an event that includes events that are in both this set and `other`.

func (EventSet) IsEmpty 

func (es EventSet) IsEmpty() bool

IsEmpty returns whether this event set contains any events.

func (EventSet) String 

func (es EventSet) String() string

func (*EventSet) Subtract 

func (es *EventSet) Subtract(other EventSet)

Subtract removes events from this event set that are in another.

func (EventSet) Union 

func (es EventSet) Union(other EventSet) EventSet

Union returns an event that includes events that are in either this set and `other`.

type Loggable 

type Loggable interface {
	Logf(msg string, args ...any)
}

type Precedence 

type Precedence int

Precedence defines a standard precedence order for CSP processes.

type Process 

type Process interface {
	// Initials returns the set of events that the process is willing to perform
	// in its current state.
	Initials() EventSet

	// Perform allows the process to perform any of the events in a set, and
	// invokes a callback with each possible “after” process.  (An after process
	// describes the behavior that occurs after one of those events is
	// performed.)
	//
	// If the process cannot perform any of the events in the set, the callback
	// will not be invoked.  The callback might be invoked multiple times if
	// there is more than one possible after process — this expresses
	// nondeterminism, where it could be any of the multiple after processes,
	// and we don't yet know which one it is.
	//
	// If at any point your callback returns false, then it will not be called
	// anymore, even if there the process has additional after processes.
	// Perform itself returns false if your callback ever returns false.
	Perform(events EventSet, callback ProcessCallback) bool

	// Precedence returns the precedence of this process.
	Precedence() Precedence
	// contains filtered or unexported methods
}

Process represents a CSP process.

A CSP process is defined by what events it's willing and able to communicate, and when.

func AftersForProcesses 

func AftersForProcesses(processes []Process, events EventSet) []Process

AftersForProcesses takes in a list of processes, checks to see which ones can perform a particular set of events, and returns the list of processes that we might be after any of those events are performed.

func ExternalChoice 

func ExternalChoice(subprocesses ...Process) Process

ExternalChoice returns a process that lets the environment choose between one of its inputs.

func Hide 

func Hide(pp Process, hidden EventSet) Process

Hide returns a process that acts exactly like another process, but with all events in a set hidden.

func Interleave 

func Interleave(subprocesses ...Process) Process

Interleave returns a process that allows all of its inputs to run independently of each other.

func InternalChoice 

func InternalChoice(subprocesses ...Process) Process

InternalChoice returns a process that nondeterministically behaves like one of its inputs.

func Parallel 

func Parallel(synchronized EventSet, lhs Process, rhs Process) Process

Parallel returns a process that allows each of its inputs to run concurrently, synchronizing on the events in a given set.

func Prefix 

func Prefix(initials EventSet, after Process) Process

Prefix returns a process that performs any event in a set, and then behaves like another process.

func Recursive 

func Recursive(name string, construct func(reference Process) Process) Process

Recursive returns a process that can be defined recursively in terms of itself. You provide a function that constructs the recursive process given a reference to itself.

func RecursiveBody 

func RecursiveBody(process Process) Process

RecursiveBody checks whether a process is a recursive definition, and if so, returns the process that defines the body of the recursion. Returns nil otherwise.

func RecursiveReference 

func RecursiveReference(process Process) Process

RecursiveReference checks whether a process is a reference to a recursive definition, and if so, returns the recursive definition that it points to. Returns nil otherwise.

func RewriteProcess 

func RewriteProcess(p Process, t ProcessTranslation) Process

RewriteProcess transforms a process by applying a function to each child process. Whenever your function returns a non-nil value, that portion of the process tree is replaced with the result.

func SequentialComposition 

func SequentialComposition(p Process, q Process) Process

SequentialComposition returns a process that behaves like process P until it performs a ✔ event, after which is behaves like process Q.

func Skip 

func Skip() Process

Skip returns a process that performs no actions (and prevents any other synchronized processes from performing any, either).

func Stop 

func Stop() Process

Stop returns a process that performs no actions (and prevents any other synchronized processes from performing any, either).

type ProcessCallback 

type ProcessCallback func(Process) bool

ProcessCallback is a callback that is invoked for one or more processes.

type ProcessTranslation 

type ProcessTranslation func(Process) Process

ProcessTranslation is a callback that optionally replaces a process with another. It should return nil if the process should remain unchanged.

type Trace 

type Trace struct {
	// contains filtered or unexported fields
}

Trace is a sequence of events.

func NewTrace 

func NewTrace(events ...Event) Trace

NewTrace creates a new Trace that consists of the given slice of events.

func (Trace) AsSlice 

func (t Trace) AsSlice() []Event

AsSlice returns the events in this trace as a slice.

func (Trace) Equals 

func (t Trace) Equals(other Trace) bool

Equals returns whether two traces are equal.

func (Trace) Format 

func (t Trace) Format(f fmt.State, verb rune)

func (Trace) String 

func (t Trace) String() string

type TraceChecker 

type TraceChecker struct {
	Actual   TracedProcess
	Expected TracedProcess
}

TraceChecker checks a limited form of traces equivalence in our test cases. We are given two processes, and want to verify that they have the same set of (possibly infinite!) traces. Instead of performing a brute-force check of every trace, we use a source of randomness (from the property check framework) to select a single trace, and verify that both processes satisfy it. (That means we rely on running our property tests against a large enough number of cases to fully explore the state space of whatever processes we create.)

func NewTraceChecker 

func NewTraceChecker(actual Process, expected Process) TraceChecker

NewTraceChecker creates a new trace checker for the given pair of processes. Since this is meant to be used in test cases, we call the two processes “actual” and “expected”.

func (*TraceChecker) Perform 

func (tc *TraceChecker) Perform(e Event) error

Perform ensures that both processes can perform an event.

func (*TraceChecker) RequireEqualInitials 

func (tc *TraceChecker) RequireEqualInitials() (EventSet, error)

RequireEqualInitials verifies that the “actual” and “expected” processes have the same set of allowed events at this point in the test.

type TraceCounterexample 

type TraceCounterexample struct {
	Process Process
	Trace   Trace
	Next    Event
}

TraceCounterexample indicates that a process cannot perform a particular trace. It includes the prefix of the trace that _could_ be performed, along with the event that it should have been able to perform next.

func (*TraceCounterexample) Error 

func (tce *TraceCounterexample) Error() string

func (*TraceCounterexample) Format 

func (tce *TraceCounterexample) Format(f fmt.State, verb rune)

func (*TraceCounterexample) String 

func (tce *TraceCounterexample) String() string

type TracedProcess 

type TracedProcess struct {
	Label    string
	Original Process
	Current  []Process
	Events   []Event
}

func NewTracedProcess 

func NewTracedProcess(label string, p Process) TracedProcess

NewTracedProcess creates a new process that we can track traces for.

func (*TracedProcess) Initials 

func (tp *TracedProcess) Initials() EventSet

Initials returns the set of events that the process is able to perform at this point in the test.

func (*TracedProcess) Log 

func (tp *TracedProcess) Log(t Loggable)

func (*TracedProcess) Perform 

func (tp *TracedProcess) Perform(e Event) error

Perform allows one of the processes to perform an event without performing the same event in the other process.

func (*TracedProcess) Reset 

func (tp *TracedProcess) Reset(p Process)

Reset resets this process back to a particular process definition, without losing track of which events had been performed previously. (This is useful in particular when testing recursive processes against a base case.)

func (*TracedProcess) TauClose 

func (tp *TracedProcess) TauClose()

TauClose follows any sequence τ events that the process can currently perform.

func (*TracedProcess) Trace 

func (tp *TracedProcess) Trace() Trace

Trace returns the trace of events that this process has performed so far.

type UnexpectedInitials 

type UnexpectedInitials struct {
	Actual           Process
	ActualTrace      Trace
	ActualInitials   EventSet
	Expected         Process
	ExpectedTrace    Trace
	ExpectedInitials EventSet
}

UnexpectedInitials indicates that two processes should have the same set of initial events after a particular trace, but do not.

func (*UnexpectedInitials) Error 

func (ui *UnexpectedInitials) Error() string

func (*UnexpectedInitials) Format 

func (ui *UnexpectedInitials) Format(f fmt.State, verb rune)

func (*UnexpectedInitials) String 

func (ui *UnexpectedInitials) String() string

type UserEventSet 

type UserEventSet interface {
	// Contains returns whether this event set contains a particular event.
	Contains(event any) bool

	// Difference returns an event set that includes events that are in this
	// event set but not in `other`.
	Difference(other UserEventSet) UserEventSet

	// Equal returns whether two event sets are equal.
	Equal(other UserEventSet) bool

	// HasNonemptyIntersection returns whether there are any events that are
	// both in this event set and another.
	HasNonemptyIntersection(other UserEventSet) bool

	// Intersection returns an event that includes events that are in both this
	// set and `other`.
	Intersection(other UserEventSet) UserEventSet

	// IsEmpty returns whether this event set contains any events.
	IsEmpty() bool

	// Union returns an event that includes events that are in either this set
	// and `other`.
	Union(other UserEventSet) UserEventSet
}

UserEventSet is a set of user events—that is, any events other than the builtin τ and ✔ events.

Source Files

View all Source files

Directories

Path Synopsis
Package cspslog collects and validates slog records as CSP traces
 Package cspslog collects and validates slog records as CSP traces
cspslogtest

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.