// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php
// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2"

action done;

// constants
const int N = 6;
const int K = 4;
const int range = 2 * (K + 1) * N;
const int counter_init = (K + 1) * N;
const int left = N;
const int right = 2 * (K + 1) * N - N;

// shared coin
int(0..range) counter = counter_init;
reward coin_flips;

property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1;
property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1));

int(0..1) fin1, fin2, fin3, fin4, fin5, fin6;
int(0..1) coin1, coin2, coin3, coin4, coin5, coin6;

process Tourist1()
{
	process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin1 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished()
		::	when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished()
		::	when(counter > left && counter < right) Tourist1()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

process Tourist2()
{
	process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin2 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished()
		::	when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished()
		::	when(counter > left && counter < right) Tourist2()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

process Tourist3()
{
	process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin3 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished()
		::	when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished()
		::	when(counter > left && counter < right) Tourist3()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

process Tourist4()
{
	process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin4 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished()
		::	when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished()
		::	when(counter > left && counter < right) Tourist4()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

process Tourist5()
{
	process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin5 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished()
		::	when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished()
		::	when(counter > left && counter < right) Tourist5()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

process Tourist6()
{
	process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() }
	process Write() {
		alt {
		::	when(coin6 == 0 && counter > 0) {= counter-- =}; Check()
		::	when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check()
		}
	}
	process Check() {
		alt {
		::	when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished()
		::	when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished()
		::	when(counter > left && counter < right)  Tourist6()
		}
	}
	process Finished() { done; Finished() }

	Flip()
}

par {
::	Tourist1()
::	Tourist2()
::	Tourist3()
::	Tourist4()
::	Tourist5()
::	Tourist6()
}