deathstarNotEasy: CONTEXT = 
BEGIN
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% starship without any modules!

	% egysegek tipusai
 	pilotsType: TYPE = [0..3];
 	rohamosztagType: TYPE = [0..3];
	diplomataType: TYPE = [0..3];
 	karbantartoType: TYPE = [0..2];
 	rendfenntartoType: TYPE = [0..5];
 
	% a jobok es a lazado bazisok maximalis szama
 	MaxLazadoB: NATURAL = 5;
	MaxJobs: NATURAL = 5;

 	state: TYPE = {not_running, rendfenntartas, lazado_bazis_felszamolas, 
                       titkos_kuldetes, haboru_idegen_fajjal, diplomacia};
 	result: TYPE = {noop, siker, sikertelen};


 	jobsIdx: TYPE = [1..MaxJobs];

  	%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  	% push the counter for vader
  	%%%%%%%%%%%%
  	update_vader(v: BOOLEAN, v_c: [0..5]): [0..5] =
     	  IF v AND v_c /= 5 THEN v_c + 1
	  ELSE v_c ENDIF;

  	main: MODULE =
 	BEGIN
  		LOCAL
    		pilots: pilotsType,
    		rohamosztag: rohamosztagType,
    		diplomatak: diplomataType,
    		karbantartok: karbantartoType,
    		rendfenntartok: rendfenntartoType,
    		lazado_bazisok: [0..MaxLazadoB],
    		vader_is_on_base: BOOLEAN,
    		flag: array jobsIdx of BOOLEAN,
    		vader_jobs: [0..5],
    		tasks: array jobsIdx of state,
		helper: result,
            	tasks_result: array jobsIdx of result 
		
		INITIALIZATION
			% kezdetben a taskok nem futnak!
    		tasks = [[i:jobsIdx] not_running];
            tasks_result = [[i:jobsIdx] noop];

    		% kezdeti egysegek szama
    		pilots 			= 2;
    		rohamosztag 	= 3;
    		diplomatak 		= 3;
    		karbantartok 	= 2;
    		rendfenntartok 	= 5;

			% kezdeti lazado bazisok szama
    		lazado_bazisok = 0;

			% vader kezdetben nincs a bazison
    		vader_is_on_base = FALSE;
    		vader_jobs = 0;

    		flag = [[i: jobsIdx] FALSE];
			helper in {n:result | n /= noop};	
		TRANSITION
  		[
		%%%%%%%%%%%%%%%%%%%%%%%%%%%% vader tranziccioi %%%%%%%%%%%%%%%%%%%%%%%%%%%% 
       	 vader_comes:
   			NOT vader_is_on_base 
       			--> vader_is_on_base' = TRUE;
			    pilots' = pilots + 1
       		[]
       		  vader_goes:
          		vader_is_on_base AND pilots /= 0 AND vader_jobs = 5
          		--> pilots' = pilots - 1;
	      		    vader_is_on_base' = FALSE;
	      		    vader_jobs' = 0
        	[]
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


		%%%%% Adot feladttipusok megkezdeset megvalosito tranziciok %%%%%%%%%%%%%%%%
    		  ([] (i: jobsIdx):
			rendfenntartas: 
	    		  tasks[i] = not_running AND rohamosztag /= 0
	    		  --> tasks' = tasks WITH [i] := rendfenntartas;
			      tasks_result'[i] = 
			helper;
% IF lazado_bazisok = MaxLazadoB THEN siker ELSE helper ENDIF;
	        	      rohamosztag' = rohamosztag - 1)
		[]
		  ([] (i: jobsIdx):
			lazado_bazis_felszamolasa:
		    	  tasks[i] = not_running AND pilots /= 0 AND rohamosztag /= 0 AND lazado_bazisok /= 0
			  --> tasks' = tasks WITH [i] := lazado_bazis_felszamolas;
  			      tasks_result' = tasks_result WITH [i] := helper;
			      rohamosztag' = rohamosztag - 1;
			      pilots' = pilots -1;
			      lazado_bazisok' = lazado_bazisok -1)
		[]
  	          ([] (i: jobsIdx):
			diplomaciai_Kapcs_felvetel:
			  tasks[i] = not_running AND diplomatak /= 0
			  --> tasks' = tasks WITH [i] := diplomacia;
  			      tasks_result' = tasks_result WITH [i] := helper;
			      diplomatak' = diplomatak - 1)
		[]
		  ([] (i: jobsIdx): 
	            titkos_kuldetes:
		    	tasks[i] = not_running AND pilots /= 0 AND rohamosztag /= 0 AND diplomatak /= 0 AND karbantartok /= 0 AND rendfenntartok /= 0 
	            	--> tasks' = tasks WITH [i] := titkos_kuldetes;
			    tasks_result' = tasks_result WITH [i] := helper;
	              	    pilots' = pilots - 1;
	              	    rohamosztag' = rohamosztag - 1;
		      	    diplomatak' = diplomatak - 1;
	              	    karbantartok' =  karbantartok - 1;
		      	    rendfenntartok' = rendfenntartok - 1)
		[]
		  ([] (i: jobsIdx):
	            haboru_idegen_fajjal:
	             tasks[i] = not_running AND ( (1 < rohamosztag) OR (vader_is_on_base AND 1 <= rohamosztag ) ) 
		     AND 1 < pilots AND karbantartok /= 0
	             --> tasks' = tasks WITH [i] := haboru_idegen_fajjal;
 		         tasks_result' = tasks_result WITH [i] := helper;
	                 flag'[i] = IF vader_is_on_base THEN TRUE ELSE FALSE ENDIF;
	                 rohamosztag' = IF vader_is_on_base THEN rohamosztag - 1
	                                ELSE rohamosztag - 2 ENDIF;
	                 pilots' = pilots - 2;
	                 karbantartok' = karbantartok - 1)
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		
		%%%%%%%%%%%%%%%%%%%%%%% feladatok lezarasa %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		[]
		 ([] (i: jobsIdx):
	           sikeres_diplomacia:
	            tasks[i] = diplomacia AND tasks_result[i] = siker AND rendfenntartok /= 0
	            --> diplomatak' = diplomatak + 1;
		       	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
	        []
	         ([] (i: jobsIdx):
	           sikertelen_diplomacia_titkos:
	            tasks[i] = diplomacia AND tasks_result[i] = sikertelen 
		    AND pilots /= 0 AND rohamosztag /= 0 AND diplomatak /= 0 
		    AND karbantartok /= 0 AND rendfenntartok /= 0 
	            --> tasks' = tasks WITH [i] := titkos_kuldetes;
 		        tasks_result' = tasks_result WITH [i] := helper;
	              	pilots' = pilots - 1;
	              	rohamosztag' = rohamosztag - 1;
		      	diplomatak' = diplomatak - 1;
	              	karbantartok' =  karbantartok - 1;
		      	rendfenntartok' = rendfenntartok - 1)
	        []
	         ([] (i: jobsIdx):
	           sikertelen_diplomacia_haboru:
	            tasks[i] = diplomacia AND tasks_result[i] = sikertelen
		    AND ( (1 < rohamosztag) OR (vader_is_on_base AND 1 <= rohamosztag ) ) 
		    AND 1 < pilots AND karbantartok /= 0
	            -->  tasks' = tasks WITH [i] := haboru_idegen_fajjal;
 		         tasks_result' = tasks_result WITH [i] := helper;
	                 flag'[i] = IF vader_is_on_base THEN TRUE ELSE FALSE ENDIF;
	                 rohamosztag' = IF vader_is_on_base THEN rohamosztag - 1
	                                ELSE rohamosztag - 2 ENDIF;
	                 pilots' = pilots - 2;
	                 karbantartok' = karbantartok - 1;
			 diplomatak' = diplomatak + 1)   
	        []
	         ([] (i: jobsIdx):
	           sikeres_titkos_kuldetes:
	            tasks[i] = titkos_kuldetes AND tasks_result[i] = siker AND rendfenntartok /= 0
	            --> pilots' = pilots + 1;
	                rohamosztag' = rohamosztag + 1;
		       	diplomatak' = diplomatak + 1;
	                karbantartok' =  karbantartok + 1;
		       	rendfenntartok' = rendfenntartok + 1;
	                lazado_bazisok' = lazado_bazisok + 1;		
		       	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
	        []
	         ([] (i: jobsIdx):
	           sikertelen_titkos_kuldetes:
	           tasks[i] = titkos_kuldetes AND tasks_result[i] = sikertelen 
	            --> pilots' = pilots + 1;
	                rohamosztag' = rohamosztag + 1;
		       	diplomatak' = diplomatak + 1;
	                karbantartok' =  karbantartok + 1;
		       	rendfenntartok' = rendfenntartok + 1;
		       	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
	        []
	         ([] (i: jobsIdx):
	           haboru_idegen_fajjal_kis_javitas:
	            tasks[i] = haboru_idegen_fajjal AND tasks_result[i] = siker AND rendfenntartok /= 0
	            --> rohamosztag' = IF flag[i] THEN rohamosztag + 1
		 		       ELSE rohamosztag + 2 ENDIF;
	                pilots' = pilots + 2;
	                karbantartok' = karbantartok + 1;
	                flag'[i] = FALSE;
		        tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
		[]
		 ([] (i: jobsIdx):
	           haboru_idegen_fajjal_nagy_javitas:
	            tasks[i] = haboru_idegen_fajjal AND tasks_result[i] = sikertelen AND rendfenntartok /= 0 
	            AND (karbantartok /= 0 OR vader_is_on_base = TRUE)
	            --> rohamosztag' = IF flag[i] THEN rohamosztag + 1
		   		       ELSE rohamosztag + 2 ENDIF;
	                pilots' = pilots + 2;
	                karbantartok' = karbantartok + 1;
	                flag'[i] = FALSE;
		        tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
		[]
	         ([] (i: jobsIdx):
	           lazado_bazis_leigazas_javitas_nelkul:
	            tasks[i] = lazado_bazis_felszamolas AND tasks_result[i] = siker AND rendfenntartok /= 0
	            --> rohamosztag' = rohamosztag + 1;
			pilots' = pilots + 1;
		       	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
		[]
	         ([] (i: jobsIdx):
	           lazado_bazis_leigazas_javitassal:
	            tasks[i] = lazado_bazis_felszamolas AND tasks_result[i] = sikertelen AND rendfenntartok /= 0
	            AND karbantartok /= 0
	            --> rohamosztag' = rohamosztag + 1;
			pilots' = pilots + 1;
		       	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
		[]
	         ([] (i: jobsIdx):
	           sikeres_rendfenntartas:
	            tasks[i] = rendfenntartas AND tasks_result[i] = siker AND rendfenntartok /= 0
	            --> rohamosztag' = rohamosztag + 1;
	        	tasks' = tasks WITH [i] := not_running;
			tasks_result' = tasks_result WITH [i] := noop;
			vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
		[]
	     ([] (i: jobsIdx):
	        sikertelen_rendfenntartas:
	           tasks[i] = rendfenntartas AND tasks_result[i] = sikertelen AND lazado_bazisok < 5
	           --> rohamosztag' = rohamosztag + 1;
		 		   tasks' = tasks WITH [i] := not_running;
				   tasks_result' = tasks_result WITH [i] := noop;			
		       	   lazado_bazisok' = lazado_bazisok + 1;
				   vader_jobs' = update_vader(vader_is_on_base, vader_jobs))
  		]
	END;


        stateSzam(tasks: array jobsIdx of state, jobCnt: jobsIdx, typeOfstate: state, sum: NATURAL): NATURAL = 
	    IF jobCnt = 0 THEN
			sum
 	    ELSE
              IF (tasks[jobCnt] = typeOfstate) THEN
	   	stateSzam(tasks, jobCnt - 1, typeOfstate, sum + 1)
	      ELSE
	        stateSzam(tasks, jobCnt - 1, typeOfstate, sum)
	      ENDIF
	    ENDIF;
	
	    numOfRunningJobs(tasks: array jobsIdx of state, jobCnt: jobsIdx, sum: NATURAL): NATURAL =
	    IF jobCnt = 0 THEN
			sum
		ELSE
			IF (tasks[jobCnt] /= not_running) THEN
				numOfRunningJobs(tasks, jobCnt - 1, sum + 1)
			ELSE
				numOfRunningJobs(tasks, jobCnt - 1, sum)
			ENDIF
		ENDIF;
noDead9: THEOREM main |-
(
	G( (numOfRunningJobs(tasks, MaxJobs, 0) = 5 ) =>
	    (F((EXISTS (i: jobsIdx): tasks[i] = not_running)) )
	 )
);

 
%%%% 2. a rendszer fair, barmely feladatot el tudja vegezni a halalcsillag
fairSystem: THEOREM main |- 
(
   FORALL (j: jobsIdx): (tasks[j] /= not_running) => F(tasks[j] = not_running)
);
%%%% 3.
varakozasiSor: THEOREM main |-
(
	G(FORALL (i:jobsIdx):
		F( (tasks[i] /= not_running) => X(tasks[i] /= not_running) )
	 )

);

%%%% 4. RENDFENNTARTO ROBOTOK SOSEM FOGYNAK EL A HALALCSILLAGON
rendfenntartok: THEOREM main |- G( 0 < rendfenntartok );

END