***
*** Simple coin toss example
***
*** It is intended to be used with the umaudemc's pcheck command
***

mod COIN is
	sort Coin .
	ops head tail : -> Coin [ctor] .

	vars C C' : Coin .

	rl [thead] : C => head [metadata "8"] .
	rl [ttail] : C => tail [metadata "5"] .
endm

smod COIN-STRAT is
	protecting COIN .
	protecting NAT .

	strats repeat : Nat @ Coin .

	var N : Nat .

	strat toss @ Coin .
	sd toss := thead | ttail .

	sd repeat(0) := idle .
	sd repeat(s(N)) := toss ; repeat(N) .
endsm

sload model-checker

mod COIN-PREDS is
	protecting COIN .
	including SATISFACTION .

	subsorts Coin < State Prop .

	vars C C' : Coin .

	eq C |= C' = C == C' .
endm

smod COIN-SCHECK is
	protecting COIN-STRAT .
	protecting COIN-PREDS .
	including MODEL-CHECKER .
	including STRATEGY-MODEL-CHECKER .

	vars C C' L R : Coin .
	var  Q A      : Qid .

	*** inertia can be used with the term assignment method of umaudemc's
	*** pcheck to specify that obtaining the same face in the next toss
	*** is twice as likely as obtaining a different one

	op inertia : Coin Coin -> Nat .
	eq inertia(C, C') = if C == C' then 2 else 1 fi .
endsm

*** Properties under different assignment methods

*** umaudemc pcheck coin head '[] <= 4 head'
*** Result: 0.0625
*** umaudemc pcheck coin head '[] <= 4 head' --assign metadata
*** Result: 0.1434123455061096
*** umaudemc pcheck coin head '[] <= 4 head' --assign 'uaction(thead=8, ttail=5)'
*** Result: 0.1434123455061096
*** umaudemc pcheck coin head '[] <= 4 head' --assign 'term(inertia(L, R))'
*** Result: 0.19753086419753085

*** umaudemc pcheck coin head '<> tail' --step
*** Result: 2.0
*** umaudemc pcheck coin head '<> tail' --step --assign metadata
*** Result: 2.5999999999999996

*** umaudemc scheck coin head coin.multiquatex --assign metadata