iriyak

var process_P = [
	["P0", ["lock", "P1", function (r) { return r.mutex == 0 },
		function (r) { r.mutex = 1 }]],
	["P1", ["read", "P2", function (r) { return true },
		function (r) { r.t1 = r.x }]],
	["P2", ["inc", "P3", function (r) { return true },
		function (r) { r.t1 = r.t1 + 1 }]],
	["P3", ["write", "P4", function (r) { return true },
		function (r) { r.x = r.t1 }]],
	["P4", ["unlock", "P5", function (r) { return true },

ryohji

package app

fun main() {
    val rules: List<Rule> = listOf(
        object : Rule {
            override val name = "read"
            override fun applicable(shared: Shared, thread: Thread) = thread.ir == Location.P0
            override fun convert(shared: Shared, thread: Thread) = shared to Local(Location.P1, shared.x)
        },
        object : Rule {

iriyak

var process_P = [
	["P0", ["read", "P1", function (r) { return true },
		function (r) { r.t1 = r.x }]],
	["P1", ["inc", "P2", function (r) { return true },
		function (r) { r.t1 = r.t1 + 1 }]],
	["P2", ["write", "P3", function (r) { return true },
		function (r) { r.x = r.t1 }]],
	["P3", []]
];

ept

theory
  Consensus_Demo
imports
  Network
begin

datatype 'val msg
  = Propose 'val
  | Accept 'val