Add support for nondeterministic specifications

model.go

@@ -1,6 +1,9 @@
 package porcupine
 
-import "fmt"
+import (
+	"fmt"
+	"strings"
+)
 
 // An Operation is an element of a history.
 //
@@ -89,6 +92,133 @@ type Model struct {
 	DescribeState func(state interface{}) string
 }
 
+// A NondeterministicModel is a nondeterministic sequential specification of a
+// system.
+//
+// For basics on models, see the documentation for [Model].  In contrast to
+// Model, NondeterministicModel has a step function that returns a set of
+// states, indicating all possible next states. It can be converted to a Model
+// using the [NondeterministicModel.ToModel] function.
+//
+// It may be helpful to look at this package's [test code] for examples of how
+// to write and use nondeterministic models.
+//
+// [test code]: https://github.com/anishathalye/porcupine/blob/master/porcupine_test.go
+type NondeterministicModel struct {
+	// Partition functions, such that a history is linearizable if and only
+	// if each partition is linearizable. If left nil, this package will
+	// skip partitioning.
+	Partition      func(history []Operation) [][]Operation
+	PartitionEvent func(history []Event) [][]Event
+	// Initial states of the system.
+	Init func() []interface{}
+	// Step function for the system. Returns all possible next states for
+	// the given state, input, and output. If the system cannot step with
+	// the given state/input to produce the given output, this function
+	// should return an empty slice.
+	Step func(state interface{}, input interface{}, output interface{}) []interface{}
+	// Equality on states. If left nil, this package will use == as a
+	// fallback ([ShallowEqual]).
+	Equal func(state1, state2 interface{}) bool
+	// For visualization, describe an operation as a string. For example,
+	// "Get('x') -> 'y'". Can be omitted if you're not producing
+	// visualizations.
+	DescribeOperation func(input interface{}, output interface{}) string
+	// For visualization purposes, describe a state as a string. For
+	// example, "{'x' -> 'y', 'z' -> 'w'}". Can be omitted if you're not
+	// producing visualizations.
+	DescribeState func(state interface{}) string
+}
+
+func merge(states []interface{}, eq func(state1, state2 interface{}) bool) []interface{} {
+	var uniqueStates []interface{}
+	for _, state := range states {
+		unique := true
+		for _, us := range uniqueStates {
+			if eq(state, us) {
+				unique = false
+				break
+			}
+		}
+		if unique {
+			uniqueStates = append(uniqueStates, state)
+		}
+	}
+	return uniqueStates
+}
+
+// ToModel converts a [NondeterministicModel] to a [Model] using a power set
+// construction.
+//
+// This makes it suitable for use in linearizability checking operations like
+// [CheckOperations]. This is a general construction that can be used for any
+// nondeterministic model. It relies on the NondeterministicModel's Equal
+// function to merge states. You may be able to achieve better performance by
+// implementing a Model directly.
+func (nm *NondeterministicModel) ToModel() Model {
+	// like fillDefault
+	equal := nm.Equal
+	if equal == nil {
+		equal = shallowEqual
+	}
+	describeOperation := nm.DescribeOperation
+	if describeOperation == nil {
+		describeOperation = defaultDescribeOperation
+	}
+	describeState := nm.DescribeState
+	if describeState == nil {
+		describeState = defaultDescribeState
+	}
+	return Model{
+		Partition:      nm.Partition,
+		PartitionEvent: nm.PartitionEvent,
+		// we need this wrapper to convert a []interface{} to an interface{}
+		Init: func() interface{} {
+			return merge(nm.Init(), nm.Equal)
+		},
+		Step: func(state, input, output interface{}) (bool, interface{}) {
+			states := state.([]interface{})
+			var allNextStates []interface{}
+			for _, state := range states {
+				allNextStates = append(allNextStates, nm.Step(state, input, output)...)
+			}
+			uniqueNextStates := merge(allNextStates, equal)
+			return len(uniqueNextStates) > 0, uniqueNextStates
+		},
+		// this operates on sets of states that have been merged, so we
+		// don't need to check inclusion in both directions
+		Equal: func(state1, state2 interface{}) bool {
+			states1 := state1.([]interface{})
+			states2 := state2.([]interface{})
+			if len(states1) != len(states2) {
+				return false
+			}
+			for _, s1 := range states1 {
+				found := false
+				for _, s2 := range states2 {
+					if equal(s1, s2) {
+						found = true
+						break
+					}
+				}
+				if !found {
+					return false
+				}
+			}
+			return true
+		},
+		DescribeOperation: describeOperation,
+		DescribeState: func(state interface{}) string {
+			states := state.([]interface{})
+			var descriptions []string
+			for _, state := range states {
+				descriptions = append(descriptions, describeState(state))
+			}
+			return fmt.Sprintf("{%s}", strings.Join(descriptions, ", "))
+		},
+	}
+}
+
 // noPartition is a fallback partition function that partitions the history
 // into a single partition containing all of the operations.
 func noPartition(history []Operation) [][]Operation {

porcupine_test.go

@@ -1553,3 +1553,145 @@ func TestSetModel(t *testing.T) {
 		t.Fatal("expected operations not to be linearizable")
 	}
 }
+
+// a specification for a nondeterministic register that supports a "put-any"
+// operation that writes some subset of the specified values to the register,
+// and a "get-any" operation that reads some subset of the values in the
+// register
+
+type nondeterministicRegisterState = []int
+
+type nondeterministicRegisterInput struct {
+	// put-any: op = 1
+	// get-any: op = 2
+	// get-all: op = 3
+	op    int
+	value []int
+}
+
+func subsets(v []int) []interface{} {
+	if len(v) == 0 {
+		return []interface{}{[]int{}}
+	}
+	ss := []interface{}{}
+	for _, subset := range subsets(v[1:]) {
+		ss = append(ss, subset)
+		ss = append(ss, append([]int{v[0]}, subset.([]int)...))
+	}
+	return ss
+}
+
+func setEqual(s1, s2 []int) bool {
+	for _, v1 := range s1 {
+		found := false
+		for _, v2 := range s2 {
+			if v1 == v2 {
+				found = true
+				break
+			}
+		}
+		if !found {
+			return false
+		}
+	}
+	for _, v2 := range s2 {
+		found := false
+		for _, v1 := range s1 {
+			if v1 == v2 {
+				found = true
+				break
+			}
+		}
+		if !found {
+			return false
+		}
+	}
+	return true
+}
+
+var nondeterministicRegisterModel = NondeterministicModel{
+	Init: func() []interface{} {
+		states := []interface{}{nondeterministicRegisterState{}}
+		return states
+	},
+	Step: func(state interface{}, input interface{}, output interface{}) []interface{} {
+		st := state.(nondeterministicRegisterState)
+		inp := input.(nondeterministicRegisterInput)
+		out := output.([]int)
+		if inp.op == 1 {
+			return subsets(inp.value)
+		} else if inp.op == 2 {
+			isSubset := true
+			for _, val := range out {
+				found := false
+				for _, stVal := range st {
+					if val == stVal {
+						found = true
+						break
+					}
+				}
+				if !found {
+					isSubset = false
+					break
+				}
+			}
+			if isSubset {
+				return []interface{}{st}
+			}
+			return []interface{}{}
+		} else {
+			if setEqual(st, out) {
+				return []interface{}{st}
+			}
+			return []interface{}{}
+		}
+	},
+	Equal: func(state1, state2 interface{}) bool {
+		st1 := state1.(nondeterministicRegisterState)
+		st2 := state2.(nondeterministicRegisterState)
+		return setEqual(st1, st2)
+	},
+	// step function: takes a state, input, and output, and returns all possible next states
+	DescribeOperation: func(input, output interface{}) string {
+		inp := input.(nondeterministicRegisterInput)
+		switch inp.op {
+		case 1:
+			return fmt.Sprintf("put-any(%v)", inp.value)
+		case 2:
+			return fmt.Sprintf("get-any() -> %v", output.([]int))
+		case 3:
+			return fmt.Sprintf("get-all() -> %v", output.([]int))
+		}
+		return "<invalid>" // unreachable
+	},
+}
+
+func TestNondeterministicRegisterModel(t *testing.T) {
+	events := []Event{
+		// C0: PutAny({1, 2, 3, 4})
+		{Kind: CallEvent, Value: nondeterministicRegisterInput{1, []int{1, 2, 3, 4}}, Id: 0, ClientId: 0},
+		// C1: GetAny()
+		{Kind: CallEvent, Value: nondeterministicRegisterInput{2, nil}, Id: 1, ClientId: 1},
+		// C2: GetAny()
+		{Kind: CallEvent, Value: nondeterministicRegisterInput{2, nil}, Id: 2, ClientId: 2},
+		// C3: GetAll()
+		{Kind: CallEvent, Value: nondeterministicRegisterInput{3, nil}, Id: 3, ClientId: 3},
+		// C2: Completed GetAny -> {2}
+		{Kind: ReturnEvent, Value: []int{2}, Id: 2, ClientId: 2},
+		// C1: Completed GetAny -> {1, 4}
+		{Kind: ReturnEvent, Value: []int{1, 4}, Id: 1, ClientId: 1},
+		// C1: Completed GetAll -> {1, 2, 3}
+		{Kind: ReturnEvent, Value: []int{1, 2, 3}, Id: 3, ClientId: 3},
+		// C0: Completed PutAny
+		{Kind: ReturnEvent, Value: []int{}, Id: 0, ClientId: 0},
+	}
+
+	model := nondeterministicRegisterModel.ToModel()
+	res, info := CheckEventsVerbose(model, events, 0)
+
+	if res != Illegal {
+		t.Fatal("expected operations to not be linearizable")
+	}
+
+	visualizeTempFile(t, model, info)
+}