#include "civlc.h"
#include "stdio.h"

$input int N;
$input int B;
$assume(0 <= N && N <= B);

int actual;

void f ($proc prev, int i) {
	$wait(prev);
	actual = i - actual;
}

void g (){}


int main ( void ) {

	actual = 0;
	$proc last_proc = $spawn g();
	for (int i = 0; i < N; i++)
		last_proc = $spawn f(last_proc, i);

	int expected = 0;
	for (int i = 0; i < N; i++)
		expected = i - expected;

	$wait(last_proc);
	printf("expected = %d, actual = %d\n", expected, actual);
	$assert(actual == expected);
}