CTL model checking algorithm

ctl.pas

(*

Rard, B. (2001). Systems and software verification: Model-checking techniques and tools. Berlin: Springer.

*)


procedure marking(phi)

	(* Caso de que phi sea una proposicion atomica *)
	case 1: phi = P
		for all q in Q, if P in l(q) then do q.phi := true, else do q.phi := false.

	
	(* Caso de que phi sea una negacion de psi *)
	case 2: phi = not psi
		do marking(psi);
		for all q in Q, do q.phi := not(q.psi).

	
	(* Caso de que phi sea una conjuncion de dos phi *)
	case 3: phi = psi1 /\ psi2
		do marking(psi1); marking(psi2);
		for all q in Q, do q.phi := and(q.psi1, q.psi2).

	
	(* Caso de que phi sea de la forma EX psi *)
	case 4: phi = EX psi
		do marking(psi);
		for all q in Q, do q.psi := false; 			// Inicializacion
		for all (q, q`) in T, if q`.psi = true then do q.phi := true. 

	
	(* Caso de que phi sea de la forma E psi1 U psi2 *)
	case 5: phi = E psi1 U psi2
		do marking(psi1); marking(psi2);
		for all q in Q,
			q.phi := false; q.seenbefore := false;	// Inicializacion
		L := set of Q;									// Los estados a ser procesados
		for all q in Q, if q.psi2 = true then do L := L + [q];
		while L is not empty do
			draw q from L;
			L := L - [q];
			q.phi := true;
			for all (q, q`) in T
				if q`.seenbefore = false then do
					q`.seenbefore := true;
					if q`.psi1 = true then do L := L + [q];


    
    (* Caso de que phi sea la forma A phi1 U psi2 *)
	case 6: phi = A psi1 U psi2
		do marking(psi1); marking(psi2);
		L := set of Q;							// Los estados a ser procesados
		for all q in Q,
			q.nb := degree(q); q.phi := false;  // Inicializacion

		for all q in Q, if q.psi2 = true then do L := L + [q];

		while L is not empty do
			draw q from L;
			L := L - [q];
			q.phi := true;
			for all (q, q`) in T,
				q`.nb := q`.nb - 1;
				if (q`.nb = 0) and (q`.psi1 = true) and (q`.psi2 = false)
					then do L := L + [q]