***
*** Implementation of the ninja's protocols in «Black Ninjas in the Dark:
*** Formal Analysis of Population Protocols» (10.1145/3209108.3209110).
***

mod NINJAS is
	protecting NAT .

	sorts Mode Vote Ninja Garden .
	subsort Ninja < Garden .

	ops A P : -> Mode [ctor] .
	ops Y N : -> Vote [ctor] .

	op {_,_} : Mode Vote -> Ninja [ctor] .

	op empty : -> Garden [ctor] .
	op __    : Garden Garden -> Garden [ctor assoc comm id: empty] .

	vars V W : Vote .
	vars K L : Nat .

	rl [ay&an] : {A, Y} {A, N} => {P, N} {P, N} .
	crl [a&p]  : {A, V} {P, W} => {A, V} {P, V} if V =/= W .
	rl [py&pn] : {P, Y} {P, N} => {P, N} {P, N} .

	op initial : Nat Nat -> Garden .
	eq initial(0, 0) = empty .
	eq initial(0, s K) = {A, N} initial(0, K) .
	eq initial(s K, L) = {A, Y} initial(K, L) .
endm

mod NINJAS-SENSEIII is
	extending NINJAS .

	op T : -> Vote [ctor] .	*** tie

	rl [ay&at] : {A, Y} {A, T} => {A, Y} {P, Y} .
	rl [aytan] : {A, Y} {A, N} => {A, T} {P, T} .
	rl [at&an] : {A, T} {A, N} => {A, N} {P, N} .
	rl [at&at] : {A, T} {A, T} => {A, T} {P, T} .

	*** and a&p
endm

smod NINJAS-STRAT is
	protecting NINJAS .
	protecting NINJAS-SENSEIII .

	strats sensei sensei-bis senseii senseiii @ Garden .

	sd sensei     := (ay&an | a&p) ! .
	sd sensei-bis := (ay&an or-else a&p) ! .
	sd senseii    := (ay&an | a&p | py&pn) ! .
	sd senseiii   := (ay&at | aytan | at&an | at&at | a&p) ! .
endsm

sload model-checker

mod NINJAS-PREDS is
	protecting NINJAS-SENSEIII .
	including SATISFACTION .

	subsort Garden < State .

	var  G   : Garden .
	var  M   : Mode .
	vars V W : Vote .

	*** There is a consensus for a given vote
	op consensus : Vote -> Prop [ctor] .
	*** There is a consensus (whatever it is)
	op consensus : -> Prop .

	eq G |= consensus(V) = collect(G) == V .
	eq G |= consensus = collect(G) =/= diverge .

	*** Collect the votes
	sort Vote? .
	subsort Vote < Vote? .

	*** The vote diverges
	op diverge : -> Vote? [ctor] .

	op collect : Garden -> Vote? .
	op check : Garden Vote -> Bool .

	eq collect(empty) = diverge .
	eq collect({M, V} G) = if check(G, V) then V else diverge fi .

	eq check(empty, V) = true .
	eq check({M, V} G, V) = check(G, V) .
	eq check({M, W} G, V) = false [owise] .
endm

smod NINJAS-CHECK is
	protecting NINJAS-PREDS .
	protecting NINJAS-STRAT .
	including MODEL-CHECKER .
	including STRATEGY-MODEL-CHECKER .

	vars V W : Vote .
endsm

*** srew initial(N, M) using sensei... .
*** red modelCheck(initial(N, M), <> consensus, 'sensei...) .