-- int number, i = 1, factorial = 1, sigma = 0, primes;
-- cin << number;
-- if (number > 2) { // e1
--     for (int j = 3; j <= number; j++) { // e2
--         factorial = 1; // e3
--         i = 1; // e3
--         for (int x = 0; x < j - 2; x++) { // e4
--             factorial = factorial * i; // e5
--             i++; // e6
--         }
--         sigma = sigma + (factorial - j * (factorial / j)); // e7
--     }
--     primes = -1 + sigma; // e8
--     if (number == 3) // e9
--         cout >> 2; // e10
--     else
--         cout >> primes; // e11
-- } else
--     cout >> "wrong number"; // e12

MODULE main

FROZENVAR number : 0..8;

VAR e : {e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12};
	i : 1..7;
	j : 3..9;
	x : 0..6;
	factorial : 1..720;
	sigma : 0..5;
	primes : 0..4;
	c : 0..6;
	a : 1..3;

ASSIGN
init(e) := e1;
next(e) := case
	e = e1 & (number > 2) : e2;
	e = e1 & (number <= 2) : e12;
	e = e2 & (j <= number) : e3;
	e = e2 & (j > number) : e8;
	e = e3 : e4;
	e = e4 & (x < ( j - 2 )) : e5;
	e = e4 & (x >= ( j - 2 )) : e7;
	e = e5 : e6;
	e = e6 : e4;
	e = e7 : e2;
	e = e8 : e9;
	e = e9 & number = 3 : e10;
	e = e9 & number != 3 : e11;
	TRUE : e;
esac;

ASSIGN
init(i) := 1;
next(i) := case
	next(e) = e3 : 1;
	next(e) = e6 & i < 2 : i + 1;
	TRUE : i;
esac;

ASSIGN
init(j) := 3;
next(j) := case
	e = e7 & next(e) = e2 & j <= 8 : j + 1;
	TRUE : j;
esac;

ASSIGN
next(x) := case
	e = e3 & next(e) = e4 : 0;
	e = e6 & next(e) = e4 & x + 1 <= 6 : x + 1;
	TRUE : x;
esac;


ASSIGN
init(factorial) := 1;
next(factorial) := case
	e = e3 : 1;
	e = e5 & factorial <= 720 & factorial*i <= 720 : factorial * i;
	TRUE: factorial;
esac;


ASSIGN
init(sigma) := 0;
next(sigma):= case
	e = e7 & (sigma + (factorial - j * (factorial / j))) <= 5 : sigma + (factorial - j * (factorial / j));
	TRUE : sigma;
esac;

ASSIGN
init(primes) := 0;
next(primes) := case
	e = e8 & (-1 + sigma) >= 0 & (-1 + sigma) <= 4 : -1 + sigma;
	TRUE : primes;
esac;

ASSIGN
init(c) := 0;
next(c) := case
	c + 1 > 6 : c;
	next(e) = e3 : c + 1;
	TRUE : c;
esac;

ASSIGN
init(a) := 1;
next(a) := case
	a = 1 & e = next(e) & i = next(i) & j = next(j) & x = next(x) & factorial = next(factorial) & sigma = next(sigma) & primes = next(primes) & c = next(c) : 2;
	a = 2 : 3;
	TRUE : a;
esac;

CTLSPEC AG (number in 0..2) <-> AX e = e12;
CTLSPEC number = 0 -> AF primes = 0;
CTLSPEC number = 8 -> AF primes = 4;
COMPUTE MAX[number = 5 & a = 1, a = 2];
CTLSPEC !EBF 35..35 (a=2);
COMPUTE MAX[number = 4 & a = 1, a=2];
CTLSPEC !EBF 22..22 (a=2);
COMPUTE MAX[number = 8 & a = 1, a=2];
CTLSPEC !EBF 92..92 (a=2);

-- -- UWAGI!!!!!!!!!
-- Dodać zmienna dodatkowa do zliczania 'j'
-- Rozlaczanie połączenia przez sesje musi być wcześniej (next w kliencie)
-- Inicjalizacja 'i' wczesniej
-- Walidacje:
-- Źle - w walidacji 0:8 nie zgadywac, użyć jakoś compute min max
-- W ostatniej walidacji nie postawiac zmiennej tylko zapisać to w formule