Practica 2: Ejecución Simbolica Dinámica

Iteración	Input concreto	Condición de ruta	Formula enviada al demostrador	Resultado posible

Untitled

Iteración	Input concreto	Condición de ruta	Formula enviada al demostrador	Resultado posible
0	a=0,b=0,c=0	C1	¬C1	a=0,b=0,c=1
1	a=0,b=0,c=1	¬C1^¬C2	¬C1^C2	a=0,b=0,c=-1
2	a=0,b=0,c=-1	¬C1^C2	END	END

Untitled

Iteración	Input concreto	Condición de ruta	Formula enviada al demostrador	Resultado posible
1	x=0, y = 0	C1 ^ ¬C2	C1 ^ C2	x = 22, y = 11
2	x=22, y = 11	C1 ^ C2	¬C1	x = 1, y = 2
3	¬C1	x = 1, y = 2	END	END

Untitled

def test_me(x):
	A = [5,7,9]
  i = 0
  if i < 3: #C1_0
	  if A[i] == x: #C2_0
			break
		i++ 
			if i < 3: #C1_1
			  if A[i] == x: #C2_1
					break
				i++
				if i < 3: #C1_2
				  if A[i] == x: #C2_2
						break
				i++
					if i < 3: #C1_2

Iteración	Input concreto	Condición de ruta	Formula enviada al demostrador	Resultado posible
1	x=0	C1_0 ^ ¬C2_0 ^ C1_1 ^ ¬C2_1 ^ C1_2 ^ ¬C2_2 ^ ¬C1_3	C1_0 ^ ¬C2_0 ^ C1_1 ^ ¬C2_1 ^ C1_2 ^ ¬C2_2 ^ C1_3	UNSAT
			C1_0 ^ ¬C2_0 ^ C1_1 ^ ¬C2_1 ^ C1_2 ^ C2_2	x = 9
2	x = 9	C1_0 ^ ¬C2_0 ^ C1_1 ^ ¬C2_1 ^ C1_2 ^ C2_2	C1_0 ^ ¬C2_0 ^ C1_1 ^ ¬C2_1 ^ ¬C1_2	UNSAT
			C1_0 ^ ¬C2_0 ^ C1_1 ^ C2_1	x=7
3	x=7	C1_0 ^ ¬C2_0 ^ C1_1 ^ C2_1	C1_0 ^ ¬C2_0 ^ ¬C1_1	UNSAT
			C1_0 ^ C2_0	x=5
4	x=5	C1_0 ^ C2_0	¬C1_0	UNSAT

Untitled