pkg/model: add register model (pingcap#10)

pkg/model/register.go

@@ -0,0 +1,57 @@
+package model
+
+import (
+	"github.com/anishathalye/porcupine"
+)
+
+// Op is an operation.
+type Op bool
+
+const (
+	// RegisterRead a register
+	RegisterRead Op = false
+	// RegisterWrite a register
+	RegisterWrite Op = true
+)
+
+// RegisterRequest is the request that is issued to a register.
+type RegisterRequest struct {
+	Op    Op
+	Value int
+}
+
+// RegisterResponse is the response returned by a register.
+type RegisterResponse struct {
+	Err   error
+	Value int
+}
+
+// RegisterModel returns a read/write register model
+func RegisterModel() porcupine.Model {
+	return porcupine.Model{
+		Init: func() interface{} {
+			state := 0
+			return state
+		},
+		Step: func(state interface{}, input interface{}, output interface{}) (bool, interface{}) {
+			st := state.(int)
+			inp := input.(RegisterRequest)
+			out := output.(RegisterResponse)
+
+			// read
+			if inp.Op == RegisterRead {
+				ok := out.Value == st || out.Err != nil
+				return ok, st
+			}
+
+			// write
+			return true, inp.Value
+		},
+
+		Equal: func(state1, state2 interface{}) bool {
+			st1 := state1.(int)
+			st2 := state2.(int)
+			return st1 == st2
+		},
+	}
+}

pkg/model/register_test.go

@@ -0,0 +1,61 @@
+package model
+
+import (
+	"testing"
+
+	"github.com/anishathalye/porcupine"
+)
+
+func TestRegisterModel(t *testing.T) {
+	// Test taken from github.com/anishathalye/porcupine
+	// examples taken from http://nil.csail.mit.edu/6.824/2017/quizzes/q2-17-ans.pdf
+	// section VII
+
+	ops := []porcupine.Operation{
+		{RegisterRequest{RegisterWrite, 100}, 0, RegisterResponse{nil, 0}, 100},
+		{RegisterRequest{RegisterRead, 0}, 25, RegisterResponse{nil, 100}, 75},
+		{RegisterRequest{RegisterRead, 0}, 30, RegisterResponse{nil, 0}, 60},
+	}
+	res := porcupine.CheckOperations(RegisterModel(), ops)
+	if res != true {
+		t.Fatal("expected operations to be linearizable")
+	}
+
+	// same example as above, but with Event
+	events := []porcupine.Event{
+		{porcupine.CallEvent, RegisterRequest{RegisterWrite, 100}, 0},
+		{porcupine.CallEvent, RegisterRequest{RegisterRead, 0}, 1},
+		{porcupine.CallEvent, RegisterRequest{RegisterRead, 0}, 2},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 0}, 2},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 100}, 1},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 0}, 0},
+	}
+	res = porcupine.CheckEvents(RegisterModel(), events)
+	if res != true {
+		t.Fatal("expected operations to be linearizable")
+	}
+
+	ops = []porcupine.Operation{
+		{RegisterRequest{RegisterWrite, 200}, 0, RegisterResponse{nil, 0}, 100},
+		{RegisterRequest{RegisterRead, 0}, 10, RegisterResponse{nil, 200}, 30},
+		{RegisterRequest{RegisterRead, 0}, 40, RegisterResponse{nil, 0}, 90},
+	}
+	res = porcupine.CheckOperations(RegisterModel(), ops)
+	if res != false {
+		t.Fatal("expected operations to not be linearizable")
+	}
+
+	// same example as above, but with Event
+	events = []porcupine.Event{
+		{porcupine.CallEvent, RegisterRequest{RegisterWrite, 200}, 0},
+		{porcupine.CallEvent, RegisterRequest{RegisterRead, 0}, 1},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 200}, 1},
+		{porcupine.CallEvent, RegisterRequest{RegisterRead, 0}, 2},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 0}, 2},
+		{porcupine.ReturnEvent, RegisterResponse{nil, 0}, 0},
+	}
+	res = porcupine.CheckEvents(RegisterModel(), events)
+	if res != false {
+		t.Fatal("expected operations to not be linearizable")
+	}
+}