package main

import "os"
import "log"
import "github.com/anishathalye/porcupine"

func visualizeTempFile(model porcupine.Model, info porcupine.LinearizationInfo) {
    file, err := os.CreateTemp("", "*.html")
    if err != nil {
        panic("failed to create temp file")
    }
    err = porcupine.Visualize(model, info, file)
    if err != nil {
        panic("visualization failed")
    }
    log.Printf("wrote visualization to %s", file.Name())
}

type registerInput struct {
    operation string // "get" and "set"
    value int
}

func main() {
    registerModel := porcupine.Model{
        Init: func() any {
            return 0
        },
        Step: func(stateAny, inputAny, outputAny any) (bool, any) {
            input := inputAny.(registerInput)
            output := outputAny.(int)
            state := stateAny.(int)
            if input.operation == "set" {
                return true, input.value
            } else if input.operation == "get" {
                readCorrectValue := output == state
                return readCorrectValue, state
            }

            panic("Unexpected operation")
        },
    }

    ops := []porcupine.Operation{
        // Client 3 sets the register to 100. The request starts at t0 and ends at t2.
        {3, registerInput{"set", 100}, 0, 100 /* end state at t2 is 100 */, 2},
        // Client 5 sets the register to 200. The request starts at t3 and ends at t4.
        {5, registerInput{"set", 200}, 3, 200/* end state at t3 is 200 */, 4},
        // Client 3 reads the register. The request starts at t5 and ends at t6.
        {3, registerInput{"get", 0 /* doesn't matter */ }, 5, 200, 6},
        // Client 5 reads the register. The request starts at t7 and ends at t8. Reads a stale value!
        {5, registerInput{"get", 0 /* doesn't matter */}, 7, 100, 8},
    }
    res, info := porcupine.CheckOperationsVerbose(registerModel, ops, 0)
    visualizeTempFile(registerModel, info)

    if res != porcupine.Ok {
        panic("expected operations to be linearizable")
    }
}

$ go mod tidy
go: finding module for package github.com/anishathalye/porcupine
go: found github.com/anishathalye/porcupine in github.com/anishathalye/porcupine v0.1.6
$ go build
$ ./lintest
2024/10/31 19:54:08 wrote visualization to /var/folders/cb/v27m749d0sj89h9ydfq0f0940000gn/T/463308000.html
panic: expected operations to be linearizable

goroutine 1 [running]:
main.main()
        /Users/phil/tmp/lintest/main.go:59 +0x394

    ops := []porcupine.Operation{
        // Client 3 sets the register to 100. The request starts at t0 and ends at t2.
        {3, registerInput{"set", 100}, 0, 100 /* end state at t2 is 100 */, 2},
        // Client 5 sets the register to 200. The request starts at t3 and ends at t4.
        {5, registerInput{"set", 200}, 3, 200/* end state at t3 is 200 */, 4},
        // Client 3 reads the register. The request starts at t5 and ends at t6.
        {3, registerInput{"get", 0 /* doesn't matter */ }, 5, 200, 6},
        // Client 5 reads the register. The request starts at t7 and ends at t8.
        {5, registerInput{"get", 0 /* doesn't matter */}, 7, 200, 8},
    }

type kvInput struct {
    operation string // "get" and "set"
    key string
    value int
}

    kvModel := porcupine.Model{
        Init: func() any {
            return map[string]int{}
        },
        Step: func(stateAny, inputAny, outputAny any) (bool, any) {
            input := inputAny.(kvInput)
            output := outputAny.(map[string]int)
            state := stateAny.(map[string]int)
            if input.operation == "set" {
                newState := map[string]int{}
                for k, v := range state {
                    newState[k] = v
                }
                newState[input.key] = input.value
                return true, newState
            } else if input.operation == "get" {
                readCorrectValue := output[input.key] == state[input.key]
                return readCorrectValue, state
            }

            panic("Unexpected operation")
        },
    }

    ops := []porcupine.Operation{
        // Client 3 set key `a` to 100. The request starts at t0 and ends at t2.
        {3, kvInput{"set", "a", 100}, 0, map[string]int{"a": 100}, 2},
        // Client 5 set key `a` to 200. The request starts at t3 and ends at t4.
        {5, kvInput{"set", "a", 200}, 3, map[string]int{"a": 200}, 4},
        // Client 3 read key `a`. The request starts at t5 and ends at t6.
        {3, kvInput{"get", "a", 0 /* doesn't matter */ }, 5, map[string]int{"a": 200}, 6},
        // Client 5 read key `a`. The request starts at t7 and ends at t8.
        {5, kvInput{"get", "a", 0 /* doesn't matter */}, 7, map[string]int{"a": 200}, 8},
    }