モデル検査器をつくる をやる

model-checking-book/example.go

@@ -0,0 +1 @@
+package main

model-checking-book/go.mod

@@ -0,0 +1,3 @@
+module github.com/uta8a/playground/model-checking-book
+
+go 1.23.4

model-checking-book/kripke.go

@@ -0,0 +1,154 @@
+package main
+
+import (
+	"fmt"
+	"hash/fnv"
+	"sort"
+	"strings"
+)
+
+type kripkeModel struct {
+	worlds     worlds
+	initial    worldID
+	accessible map[worldID][]worldID
+}
+
+type worldID uint64
+type worlds map[worldID]world
+
+func (wlds worlds) member(wld world) bool {
+	_, ok := wlds[wld.id]
+	return ok
+}
+
+func (wlds worlds) insert(wld world) {
+	wlds[wld.id] = wld
+}
+
+type world struct {
+	id              worldID
+	environment     environment
+	programCounters map[procName][]statement
+}
+
+func NewWorld(env environment, counters map[procName][]statement) world {
+	id := id(env, counters)
+	return world{id: id, environment: env, programCounters: counters}
+}
+
+func id(env environment, counters map[procName][]statement) worldID {
+	strs := []string{}
+	vnames := []string{}
+
+	for name := range env.variables {
+		vnames = append(vnames, string(name))
+	}
+	sort.Strings(vnames)
+
+	for _, name := range vnames {
+		val := env.variables[varName(name)]
+		strs = append(strs, fmt.Sprintf("%s=%d", name, val))
+	}
+
+	pnames := []string{}
+	for name := range counters {
+		pnames = append(pnames, string(name))
+	}
+	sort.Strings(pnames)
+	for _, name := range pnames {
+		stmts := counters[procName(name)]
+		strs = append(strs, fmt.Sprintf("%s=%+v", name, stmts))
+	}
+
+	hasher := fnv.New64a()
+	hasher.Write(([]byte(strings.Join(strs, ","))))
+	return worldID(hasher.Sum64())
+}
+
+func initialWorld(sys system) world {
+	vars := map[varName]int{}
+	for name, val := range sys.variables {
+		vars[name] = val
+	}
+
+	counters := map[procName][]statement{}
+	for _, proc := range sys.processes {
+		counters[proc.name] = proc.statements
+	}
+
+	newEnv := environment{
+		variables: vars,
+	}
+
+	return NewWorld(newEnv, counters)
+}
+
+func stepLocal(env environment, pname procName, stmts []statement) ([]localState, error) {
+	if len(stmts) == 0 {
+		return []localState{}, nil
+	}
+
+	return stmts[0].execute(env, pname, stmts[1:])
+}
+
+func stepGlobal(wld world) ([]world, error) {
+	wlds := []world{}
+
+	// プロセスを選ぶループ
+	for pname, stmts := range wld.programCounters {
+		states, err := stepLocal(wld.environment, pname, stmts)
+		if err != nil {
+			return []world{}, err
+		}
+		// そのプロセスの動作の可能性に対するループ
+		for _, state := range states {
+			counters := map[procName][]statement{}
+			for n, ss := range wld.programCounters {
+				if n == pname {
+					counters[n] = state.statements
+				} else {
+					counters[n] = ss
+				}
+			}
+			wld := NewWorld(state.environment, counters)
+			wlds = append(wlds, wld)
+		}
+	}
+
+	return wlds, nil
+}
+
+func KripkeModel(sys system) (kripkeModel, error) {
+	init := initialWorld(sys)
+
+	visited := worlds{}
+	visited.insert(init)
+	accs := map[worldID][]worldID{}
+
+	stack := []world{init}
+	for len(stack) > 0 {
+		current := stack[len(stack)-1]
+		stack = stack[:len(stack)-1]
+
+		acc := []worldID{}
+		nexts, err := stepGlobal(current)
+		if err != nil {
+			return kripkeModel{}, err
+		}
+		for _, next := range nexts {
+			acc = append(acc, next.id)
+
+			if !visited.member(next) {
+				visited.insert(next)
+				stack = append(stack, next)
+			}
+		}
+		accs[current.id] = acc
+	}
+
+	return kripkeModel{
+		worlds:     visited,
+		initial:    init.id,
+		accessible: accs,
+	}, nil
+}

model-checking-book/main.go

@@ -0,0 +1,18 @@
+package main
+
+import (
+	"log"
+	"os"
+)
+
+// $ go run ./...
+// 何も返ってこなければ成功
+func main() {
+	sys := Mutex()
+	model, err := KripkeModel(sys)
+	if err != nil {
+		log.Fatal(err)
+
+	}
+	model.WriteAsDot(os.Stdout)
+}

model-checking-book/mutex.dot

@@ -0,0 +1,111 @@
+digraph {
+  11221991691700317303 [label="critical=0"];
+  11221991691700317303 [ penwidth = 5 ];
+  921510197053021043 [label="critical=0"];
+  3487952452228750286 [label="critical=1"];
+  1719250695456733177 [label="critical=2"];
+  7436987335548333450 [label="critical=1"];
+  1280363200138696619 [label="critical=0"];
+  15882637993728910432 [label="critical=1"];
+  15782641524140305967 [label="critical=2"];
+  7036388809428607951 [label="critical=0"];
+  3238549733672927470 [label="critical=1"];
+  17929327978746845670 [label="critical=1"];
+  5752008125370460663 [label="critical=2"];
+  12639326343918287883 [label="critical=2"];
+  3372605456242150480 [label="critical=1"];
+  1161750338396871911 [label="critical=0"];
+  10778493553980671058 [label="critical=3"];
+  9472190305011600930 [label="critical=1"];
+  12398303882891926298 [label="critical=1"];
+  3649300105249688795 [label="critical=0"];
+  3019680412146324886 [label="critical=1"];
+  5126610833276348920 [label="critical=1"];
+  2808960358517481579 [label="critical=2"];
+  1394296989391464834 [label="critical=1"];
+  17106298229703682801 [label="critical=2"];
+  4058687436091955395 [label="critical=0"];
+  3975512886879023247 [label="critical=0"];
+  11490742439060118968 [label="critical=1"];
+  11490742439060118968 -> 15882637993728910432;
+  11490742439060118968 -> 3372605456242150480;
+  11490742439060118968 -> 11221991691700317303;
+  921510197053021043 -> 7036388809428607951;
+  921510197053021043 -> 12398303882891926298;
+  921510197053021043 -> 3649300105249688795;
+  11221991691700317303 -> 4058687436091955395;
+  11221991691700317303 -> 921510197053021043;
+  11221991691700317303 -> 3975512886879023247;
+  12398303882891926298 -> 11221991691700317303;
+  12398303882891926298 -> 17929327978746845670;
+  12398303882891926298 -> 1394296989391464834;
+  17106298229703682801 -> 3019680412146324886;
+  17106298229703682801 -> 10778493553980671058;
+  17106298229703682801 -> 17929327978746845670;
+  3487952452228750286 -> 1280363200138696619;
+  3487952452228750286 -> 5752008125370460663;
+  3487952452228750286 -> 17106298229703682801;
+  17929327978746845670 -> 3487952452228750286;
+  17929327978746845670 -> 3975512886879023247;
+  17929327978746845670 -> 2808960358517481579;
+  3019680412146324886 -> 15782641524140305967;
+  3019680412146324886 -> 3975512886879023247;
+  3019680412146324886 -> 3238549733672927470;
+  3372605456242150480 -> 921510197053021043;
+  3372605456242150480 -> 5126610833276348920;
+  3372605456242150480 -> 2808960358517481579;
+  1394296989391464834 -> 4058687436091955395;
+  1394296989391464834 -> 3487952452228750286;
+  1394296989391464834 -> 1719250695456733177;
+  5126610833276348920 -> 5752008125370460663;
+  5126610833276348920 -> 7036388809428607951;
+  5126610833276348920 -> 12639326343918287883;
+  1161750338396871911 -> 5126610833276348920;
+  1161750338396871911 -> 3238549733672927470;
+  1161750338396871911 -> 3487952452228750286;
+  15882637993728910432 -> 15782641524140305967;
+  15882637993728910432 -> 5126610833276348920;
+  15882637993728910432 -> 4058687436091955395;
+  7036388809428607951 -> 1394296989391464834;
+  7036388809428607951 -> 1161750338396871911;
+  7036388809428607951 -> 9472190305011600930;
+  5752008125370460663 -> 10778493553980671058;
+  5752008125370460663 -> 15882637993728910432;
+  5752008125370460663 -> 1394296989391464834;
+  15782641524140305967 -> 11490742439060118968;
+  15782641524140305967 -> 12639326343918287883;
+  15782641524140305967 -> 7436987335548333450;
+  4058687436091955395 -> 7036388809428607951;
+  4058687436091955395 -> 1280363200138696619;
+  4058687436091955395 -> 7436987335548333450;
+  3975512886879023247 -> 3649300105249688795;
+  3975512886879023247 -> 11490742439060118968;
+  3975512886879023247 -> 1280363200138696619;
+  3238549733672927470 -> 12639326343918287883;
+  3238549733672927470 -> 3649300105249688795;
+  3238549733672927470 -> 17106298229703682801;
+  10778493553980671058 -> 2808960358517481579;
+  10778493553980671058 -> 15782641524140305967;
+  10778493553980671058 -> 1719250695456733177;
+  9472190305011600930 -> 1719250695456733177;
+  9472190305011600930 -> 3238549733672927470;
+  9472190305011600930 -> 921510197053021043;
+  3649300105249688795 -> 3372605456242150480;
+  3649300105249688795 -> 1161750338396871911;
+  3649300105249688795 -> 17929327978746845670;
+  1280363200138696619 -> 3019680412146324886;
+  1280363200138696619 -> 1161750338396871911;
+  1280363200138696619 -> 15882637993728910432;
+  12639326343918287883 -> 10778493553980671058;
+  12639326343918287883 -> 9472190305011600930;
+  12639326343918287883 -> 3372605456242150480;
+  2808960358517481579 -> 11490742439060118968;
+  2808960358517481579 -> 12398303882891926298;
+  2808960358517481579 -> 5752008125370460663;
+  1719250695456733177 -> 7436987335548333450;
+  1719250695456733177 -> 17106298229703682801;
+  1719250695456733177 -> 12398303882891926298;
+  7436987335548333450 -> 11221991691700317303;
+  7436987335548333450 -> 9472190305011600930;
+  7436987335548333450 -> 3019680412146324886;
+}

model-checking-book/mutex.go

@@ -0,0 +1,22 @@
+package main
+
+func badThread(name procName) process {
+	return Process(name,
+		For(
+			Case(When(True()),
+				Assign("critical", Add(Var("critical"), Int(1))),
+				// critical section
+				Assign("critical", Sub(Var("critical"), Int(1))),
+			),
+		),
+	)
+}
+
+func Mutex() system {
+	return System(
+		Variables{"critical": 0},
+		badThread("A"),
+		badThread("B"),
+		badThread("C"),
+	)
+}

model-checking-book/sample.dot

@@ -0,0 +1,8 @@
+digraph {
+    1 [label="A"];
+    2 [label="B"];
+    3 [label="C"];
+    1 -> 2;
+    2 -> 3;
+    3 -> 2;
+}