Implementación del algoritmo de Tableau para la lógica temporal

Escuela Técnica Universitat Politècnica de València Implementación del algoritmo de Tableau para Escuela Técnica Superior de Ingeniería Informática Universitat Politècnica de València Implementación del algoritmo de Tableau para la lógica temporal Proyecto Fin de Carrera Ingeniería Informática Autor: Ghada El Khamlichi Director: Alicia Villanueva Valencia Superior de Ingeniería Informática Implementación del algoritmo de Tableau para Ghada El Khamlichi Alicia Villanueva Valencia 2012 El objetivo de este proyecto es de las propiedades de la lógica temporal Esto se i mplementará en el lenguaje Maude reglas Tableau que garantizan un tratamiento correcto de las eventualidades así como la completitud y la terminación del El objetivo de este proyecto es crear un método que comprueba la satisfacibilidad automática la lógica temporal lineal proposicional , mediante un algoritmo mplementará en el lenguaje Maude . El algoritmo se realizará en una pasada, y reglas Tableau que garantizan un tratamiento correcto de las eventualidades así como la y la terminación del algoritmo de satisfacibilidad. 2 Resumen método que comprueba la satisfacibilidad automática , mediante un algoritmo Tableau. realizará en una pasada, y utilizará reglas Tableau que garantizan un tratamiento correcto de las eventualidades así como la Índice de contenidos Resumen ................................ Índice ................................ ................................ Índice de contenidos ................................ Índice de figuras ................................ Índice de tablas ................................ Introducción ................................ 1. Teoría ................................ 1.1. Lógica Temporal ................................ 1.2. Método Tableau para PLTL 1.2.1. Reglas ................................ 1.2.2. Formalización del algoritmo 1.3. Maude ................................ 1.3.1. Módulos ................................ 1.3.2. Tipos (Sorts) ................................ 1.3.3. Operadores ................................ 1.3.4. Variables ................................ 1.3.5. Ecuaciones no condicionales 1.3.6. Reglas ................................ 2. Implementación y análisis 2.1. Versión simple ................................ 2.1.1. Módul o funcional 2.1.2. Tipos ................................ 2.1.3. Operadores ................................ 2.1.4. Ecuaciones ................................ 2.1.5. Funciones ................................ 2.1.6. Simplificaciones 2.1.7. Módulo de sistema ................................ ................................................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................................................ ................................ ................................ ................................................................ ................................ ................................ ................................ ................................ Método Tableau para PLTL ................................................................ .......................... ................................ ................................ ................................ Formalización del algoritmo ................................ ................................ ................................ ................................................................ ......................... ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ Ecuaciones no condicionales ................................ ................................ ................................ ................................ ................................ Implementación y análisis ................................................................ ................................ ................................ ................................ ................................ o funcional ................................................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ Simplificaciones ................................................................ ................................ Módulo de sistema ................................................................ .............................. 3 Índice ................................ ........ 2 ................................ ............. 3 ................................ ................. 3 ................................ ........................ 5 ................................ ......................... 5 ................................ .. 7 ................................ .... 9 ................................ ............ 9 .......................... 10 ................................ .................. 11 ................................ ................ 13 ......................... 16 ................................ ............... 16 ................................ ......... 17 ................................ .......... 17 ................................ .............. 17 ................................ ............... 18 ................................ .................. 18 ................................ ... 19 ................................ ............. 19 ................................ 19 ................................ .................... 19 ................................ .......... 21 ................................ ........... 24 ................................ ............ 26 ................................ ... 29 .............................. 29 2.2. Versión extendida ................................ 2.3. La importancia de los est 3. Pruebas y resultados ................................ 3.1. Ejemplo ilustrativo 3.2. Pruebas ................................ 3.2.1. Pruebas unitarias 3.2.2. Pruebas globales 3.3. Com paración de resultados 4. Conclusiones ................................ 4.1. Objetivos Conseguidos 4.2. Posibles ampliaciones Anexo ................................ ................................ Sintaxis básica de Maude ................................ Identificadores ................................ Módulos ................................ Tipos (Sorts) ................................ Operadores ................................ Variables ................................ Términos ................................ Ecuaciones no condiciona Atributos ................................ Dominio de tipo (Kind) ................................ Reglas ................................ Comandos de ejecución Código versión extendida ................................ Pruebas unitarias ................................ Bibliografía ................................ ................................ ................................ ................................ La importancia de los est ados ................................ ................................ ................................ ................................ ................................ ................................................................ ................................ ................................ ................................ ................................ Pruebas unitarias ................................................................ ................................ globales ................................................................ ................................ paración de resultados ................................ ................................ ................................ ................................ ................................ Objetivos Conseguidos ................................................................ ................................ Posibles ampliaciones ................................................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................................................ .............................. ................................ ................................................................ ......................... ................................ ................................................................ .......................... ................................ ................................................................ .............................. ................................ ................................................................ .............................. Ecuaciones no condiciona les ................................................................ ............................... ................................ ................................................................ .............................. ................................ ................................ ................................ ................................ ................................................................ ................................ ................................................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................ ................................................................ ................................ 4 ................................ ....... 29 ................................ ..................... 31 ................................ ........... 33 ................................ ...... 33 ................................ ........................ 34 ................................ . 34 ................................ . 35 ................................ ........................ 41 ................................ ....................... 45 ................................ 45 ................................ . 45 ................................ .......... 47 ................................ ........ 47 ................................ .................... 47 .............................. 47 ......................... 48 .......................... 48 .............................. 48 .............................. 49 ............................... 49 .............................. 49 ................................ ........ 49 ................................ .. 49 ................................ ...... 50 ................................ ........ 51 ................................ ..................... 55 ................................ .. 63 Índice de figuras Figura 1: Árbol para la fórmula (p U q) Figura 2: Jerarquía de los tipos Figura 3: Árbol para la fórmula F ^ q / Figura 4: Árbol para la fórmula p U false Figura 5: Árbol para la fórmula (^ q) / Figura 6: Árbol para la fórmula p / Índice de tablas Tabla 1: Reglas Tableau conjuntivas Tabla 2: Reglas Tableau disyuntivas Tabla 3: Regla Next ................................ Tabla 4: Representación de los operadores adicionales en función de los básicos Tabla 5: Reglas conjuntivas para los operadores adiciona Tabla 6: Reglas disyuntivas para los operadores adicionales Tabla 7: Representaciones de los operadores básicos Tabla 8: Comparación de la satisfacibilidad Tabla 9: Comparación del coste temporal en segundos Figura 1: Árbol para la fórmula (p U q) ∧ ¬q ................................ ................................ Figura 2: Jerarquía de los tipos ................................................................ ................................ Figura 3: Árbol para la fórmula F ^ q / \ (p U q) ................................ ................................ Figura 4: Árbol para la fórmula p U false ................................ ................................ Figura 5: Árbol para la fórmula (^ q) / \ (^ X F q) /\ (p U q) ................................ ......................... Figura 6: Árbol para la fórmula p / \ X ^ p /\ (^ false U ^ p) ................................ Tabla 1: Reglas Tableau conjuntivas ................................................................ ........................... Tabla 2: Reglas Tableau disyuntivas ................................................................ ............................ ................................ ................................ ................................ Representación de los operadores adicionales en función de los básicos Tabla 5: Reglas conjuntivas para los operadores adiciona les ................................ Tabla 6: Reglas disyuntivas para los operadores adicionales ................................ Tabla 7: Representaciones de los operadores básicos ................................ ................................ Tabla 8: Comparación de la satisfacibilidad ................................ ................................ Tabla 9: Comparación del coste temporal en segundos ................................ ............................. 5 ................................ ............... 15 ................................ ... 21 ................................ ........... 36 ................................ .................... 37 ......................... 38 ................................ ........................ 39 ........................... 11 ............................ 11 ................................ ...................... 12 Representación de los operadores adicionales en función de los básicos .................... 12 ................................ ..................... 12 ................................ ..................... 13 ................................ 21 ................................ ................ 41 ............................. 42 6 La lógica temporal es un tipo de lógica modal que fórmulas en función del tiempo muchos campos, e n particular para el análisis de los sistemas factores, determina su co mportamiento etc. Este tipo de lógica presenta aplicaciones en muchos otros campos, que abarcan desde el mundo industrial (control de procesos, robótica), de enfermedades). Existen varios métodos de decisión es el método Tableau, que consiste en fórmulas . Como resultado de la aplicación de las reglas Tableau nodos finales determinan el valor de verdad del conjunto de fórmulas de entrada A diferencia de la lógica clásica, no resulta trivial : el tratami podrían no terminar. Los algoritmos Tableau para la lógica temp donde se genera un grafo auxiliar fuertemente conectados en dicho grafo El objetivo del presente pro yecto es la implementación del tener que realizar dos pasadas, Además, se utilizan reglas que garantizan una gestión correcta de las eventualidades, y por lo tanto la terminación del mismo. lenguaje especialmente adecuado para este tipo de t intuitividad y buen rendimiento obteniendo resultados satisfactorios. La entrada del algoritmo será una fórmula de aplicando l as reglas del método de Tableau finali zación del algoritmo. Si será ciert a, de lo contrario será fórmula. La estructura de la memoria se divide introducción a las bases requeridas para entender este trabajo análisis contendrá dos versiones destacarán las principales dificultades abordadas pruebas ejecutadas para verificar la corrección del programa las diferentes versiones. Seguidamente obtenidos, junto con las dificultades presentadas a lo largo del proyecto, y las posibles ampliaciones del trabajo realizado sobre la sintaxis de l lenguaje Maude, para comprobar la corrección de Introducción un tipo de lógica modal que permite estudiar el valor de verdad de las tiempo . Hoy en día se considera una herramienta imprescindible n particular para el análisis de los sistemas donde el tiempo, entre otros mportamiento : protocolos de seguridad, sistemas en tiempo real, de lógica presenta aplicaciones en muchos otros campos, que abarcan desde el mundo industrial (control de procesos, robótica), hasta el mundo de la medicina (diagnóstico de decisión para la satisfacibilidad de las fórmulas lógica que consiste en automatizar el proceso de validación de un conjunto de . Como resultado de la aplicación de las reglas Tableau se obtiene nodos finales determinan el valor de verdad del conjunto de fórmulas de entrada A diferencia de la lógica clásica, la concepción de un algoritmo de Tableau para : el tratami ento de las eventualidades se h ace mediante ecuaciones que para la lógica temp oral clásicos funcionan en dos pasadas: u auxiliar y una posible segunda pasada para encontrar componentes en dicho grafo y verificar que sus premisas se cumplen yecto es la implementación del algoritmo definido en dos pasadas, ya que incluye todas las verificaciones en e l propio algoritmo. Además, se utilizan reglas que garantizan una gestión correcta de las eventualidades, y por lo tanto la terminación del mismo. Para la implementación se ha usado el lenguaje Maude lenguaje especialmente adecuado para este tipo de t areas ya que gracias a su simplicidad, intuitividad y buen rendimiento , permite definir fác ilmente las pasos del algoritmo de Tableau satisfactorios. La entrada del algoritmo será una fórmula de la lógica temporal proposicional line as reglas del método de Tableau sobre ésta hasta que se cumplan las condiciones de zación del algoritmo. Si se obtiene al menos un nodo abierto (de valor true) a, de lo contrario será falsa. Cada nodo fina l abierto representa un modelo para dicha La estructura de la memoria se divide en 4 partes: La sección de teoría bases requeridas para entender este trabajo ; la sección de implementación y versiones de la solución y un análisis del código de éstas destacarán las principales dificultades abordadas ; en el tercer apartado se para verificar la corrección del programa , así como una comparación Seguidamente se expondrán las conclusiones sobre los resultados obtenidos, junto con las dificultades presentadas a lo largo del proyecto, y las posibles del trabajo realizado . Finalmente, se incluye un anexo con un l lenguaje Maude, el código de la solución y las pruebas unitarias para comprobar la corrección de dicha solución. 7 Introducción el valor de verdad de las imprescindible para donde el tiempo, entre otros : protocolos de seguridad, sistemas en tiempo real, de lógica presenta aplicaciones en muchos otros campos, que abarcan desde el mundo de la medicina (diagnóstico lógica s. Uno de ellos de un conjunto de se obtiene un árbol cuyos nodos finales determinan el valor de verdad del conjunto de fórmulas de entrada . algoritmo de Tableau para la lógica modal ace mediante ecuaciones que en dos pasadas: u na primera encontrar componentes y verificar que sus premisas se cumplen . definido en (1) que evita l propio algoritmo. Además, se utilizan reglas que garantizan una gestión correcta de las eventualidades, y por lo se ha usado el lenguaje Maude , un areas ya que gracias a su simplicidad, ilmente las pasos del algoritmo de Tableau lógica temporal proposicional line al. Se irán sobre ésta hasta que se cumplan las condiciones de (de valor true) , la fórmula l abierto representa un modelo para dicha sección de teoría constituirá una sección de implementación y solución y un análisis del código de éstas , donde se en el tercer apartado se presentarán las así como una comparación entre las conclusiones sobre los resultados obtenidos, junto con las dificultades presentadas a lo largo del proyecto, y las posibles pequeño tutorial y las pruebas unitarias realizadas 8 En el siguiente apartado se exponen algoritmo por desarrollar. Se explicarán sus reglas, y finalmente se formalizar 1.1. Lógica Temporal La lógica temporal (LT) es una clase particular de la lógica modal. Se u sistemas que no tienen un final determinado o ej. sistemas concurrentes, protocolos de seguridad, hardware…). Para lógica proposicional resulta términos del tiempo. La LT permite expresar hechos como: momento en que llueva”. Dentro de la Lógica Temporal existen varias clasificacio de primer orden, ramificadas frente a lineales, disc se centra en la Lógica Temporal Proposicional L tiempo para este caso es disc de transición infinitas y que tiempo. Las fórmulas PLTL se expresan mediante los siguie • l as proposiciones atómicas • las proposiciones constante • el operador Not (¬) • los operadores And ( ∧ • l os operadores temporales:  Until (U): p U q  Next (X): X p siguiente  El operador de necesidad será cierta en todos los instantes futuros  El operador de posibilidad será cierta en algún instante futuro.  Release (R): p R q (incluido este momento). Si Las fórmulas de tipo p y ¬ p fórmulas de tipo p U q, F p Para definir la semántica formal de la lógica temporal se usa el modelo de Kriple. U e structura PLTL se representa mediante una tupla [S, R vacío de estados, R representa la función de etiquetado que define La estructura de Kriple M de una fórmula donde j >= 0. se exponen los conceptos teóricos necesarios para entender el Se explicarán las bases de la lógica temporal , el método de Tableau formalizar á el algoritmo elegido para la solución. es una clase particular de la lógica modal. Se u tiliza para analizar no tienen un final determinado o cuyo comporta miento varía con el tiempo (p. sistemas concurrentes, protocolos de seguridad, hardware…). Para este tipo de sistemas la insuficiente ya que se necesita poder expresar el sistema permite expresar hechos como: " el cielo estará despejado hasta Temporal existen varias clasificacio nes: l ógicas proposicionales frente a las de primer orden, ramificadas frente a lineales, disc retas frente a continuas, etc. la Lógica Temporal Proposicional L ineal, conocida como PLTL. La natu disc reta y lineal, es decir que se trata de una colección de secuencias que el estado del sistema se puede expresar en cada Las fórmulas PLTL se expresan mediante los siguie ntes elementos: as proposiciones atómicas (p, q…) constante s false y true ∧ ) y Or (∨) os operadores temporales: p U q se lee como p es cierta hasta el instante en que X p indica que la proposición p es cierta en el instante El operador de necesidad Globally(G): G p e xpresa que la proposición será cierta en todos los instantes futuros operador de posibilidad Eventually (F): F p expresa que la proposición será cierta en algún instante futuro. p R q se lee como q es cierto hasta el momento en que (incluido este momento). Si p nunca es cierta, q seguirá siéndolo. ¬ p , donde p es una proposición, se denominan F p y ¬ G p se llaman eventualidades. Para definir la semántica formal de la lógica temporal se usa el modelo de Kriple. U structura PLTL se representa mediante una tupla [S, R , E], donde S es un conjunto R representa la relación de la transición entre dichos estado función de etiquetado que define para cada estado qué proposiciones son ciertas de una fórmula f permite definir si ésta es cierta en un estado 9 1. Teoría los conceptos teóricos necesarios para entender el , el método de Tableau y tiliza para analizar los miento varía con el tiempo (p. este tipo de sistemas la que se necesita poder expresar el sistema en el cielo estará despejado hasta el ógicas proposicionales frente a las retas frente a continuas, etc. Este proyecto ineal, conocida como PLTL. La natu raleza del una colección de secuencias en cada instante de es cierta hasta el instante en que q sea cierta cierta en el instante de tiempo xpresa que la proposición p que la proposición p es cierto hasta el momento en que p lo sea seguirá siéndolo. se denominan literales, y las Para definir la semántica formal de la lógica temporal se usa el modelo de Kriple. U na es un conjunto finito y no estado s y E es una son ciertas . es cierta en un estado s j , 1.3. Maude El algoritmo de Tableau se ha declarativo funcional. Fue introducido Unidos . Es un lenguaje que sirve para implementar modelos de sistemas ver ificaciones formales sobre ést Maude se ha utilizado para especificar y comprobar la fiabilidad como por ejemplo el metamodelo de UML, las plataformas de CORBA y SOAP, protocolos de comunicación c omo el FireWire y Se trata de un lengua je potente en cua cualquier sistema. La otra ventaja es que su sintaxis resulta muy intuitiva, fácilmente incluso por usuarios deja más tiempo para analizar el problema. Otro aspecto importante de Maude es que soporta la lógica de reescritura, reglas permite modelar sistemas concurrentes. Esto resulta muy conveniente para el algoritmo visto ya que permite definir de forma natural A continuación se presentarán los anexo del documento se puede encontrar un tutorial completo de más útiles para manejarlo en nuestro contexto 1.3.1. Módulos Un programa Maude está compuesto por módulos. En Maude existen tres tipos de mód f uncional, de sistema y orientado a objetos. De éstos solamente El módulo funcional es donde se declaran los tipos de los datos del sistema (sorts), los operadores (ops) que son la sirven para reducir o simplificar los términos formados por los dos anteriores. Una ex de entrada será reducida por las ecuaciones del módulo funcional hasta que quede en forma canónica, es decir, cuando ya no se pueda Se declara de la siguiente manera: fmod NombreMóduloFuncional {Declaraciones del módulo} endfmod En el módulo de sistema se definen las reglas del sistema, aunque en él también se pu definir tipos, operadores y ecuaciones. Las reglas definen las transiciones que puede haber entre diferentes estados del sistema y su ej cuando los términos ya no son reducibles por las ecuaciones definidas. Se declara con la siguiente sintaxis fmod NombreMóduloSistema {Declaraciones del módulo} endfmod ha implementado en Maude. Éste es un lenguaje de programación declarativo funcional. Fue introducido y desarrollado en la universidad de Illinois en . Es un lenguaje que sirve para implementar modelos de sistemas ificaciones formales sobre ést os. ha utilizado para especificar y comprobar la fiabilidad de varios sistemas conocidos, como por ejemplo el metamodelo de UML, las plataformas de CORBA y SOAP, protocolos de omo el FireWire y el lenguaje Java. je potente en cua nto a expresividad, pues con él se puede La otra ventaja es que su sintaxis resulta muy intuitiva, y se puede entender incluso por usuarios principiantes . Esto facilita bastante la tarea de deja más tiempo para analizar el problema. Otro aspecto importante de Maude es que soporta la lógica de reescritura, sistemas concurrentes. Esto resulta muy conveniente para el algoritmo de forma natural las reglas de deducción del Tableau A continuación se presentarán los elementos más importantes de la sintaxis de Maude anexo del documento se puede encontrar un tutorial completo de l lenguaje en nuestro contexto . Un programa Maude está compuesto por módulos. En Maude existen tres tipos de mód uncional, de sistema y orientado a objetos. De éstos solamente se verán los dos primeros. funcional es donde se declaran los tipos de los datos del sistema (sorts), los operadores (ops) que son la s operaciones aplicables sobre é stos y las ecuaciones (eqs) que sirven para reducir o simplificar los términos formados por los dos anteriores. Una ex de entrada será reducida por las ecuaciones del módulo funcional hasta que quede en forma cuando ya no se pueda reducir más. manera: fmod NombreMóduloFuncional {Declaraciones del módulo} el módulo de sistema se definen las reglas del sistema, aunque en él también se pu ecuaciones. Las reglas definen las transiciones que puede haber entre diferentes estados del sistema y su ej ecución puede ser concurrente. É cuando los términos ya no son reducibles por las ecuaciones definidas. sintaxis : fmod NombreMóduloSistema {Declaraciones del módulo} 16 en Maude. Éste es un lenguaje de programación Illinois en Estados . Es un lenguaje que sirve para implementar modelos de sistemas y realizar de varios sistemas conocidos, como por ejemplo el metamodelo de UML, las plataformas de CORBA y SOAP, protocolos de nto a expresividad, pues con él se puede modelar casi y se puede entender . Esto facilita bastante la tarea de la codificación, y Otro aspecto importante de Maude es que soporta la lógica de reescritura, y gracias a sus sistemas concurrentes. Esto resulta muy conveniente para el algoritmo Tableau . sintaxis de Maude y en el l lenguaje y los comandos Un programa Maude está compuesto por módulos. En Maude existen tres tipos de mód ulos: los dos primeros. funcional es donde se declaran los tipos de los datos del sistema (sorts), los stos y las ecuaciones (eqs) que sirven para reducir o simplificar los términos formados por los dos anteriores. Una ex presión de entrada será reducida por las ecuaciones del módulo funcional hasta que quede en forma el módulo de sistema se definen las reglas del sistema, aunque en él también se pu eden ecuaciones. Las reglas definen las transiciones que puede haber ecución puede ser concurrente. É stas se aplican 1.3.2. Tipos (Sorts) Lo primero que se necesita definir en un sistema son los tipos. cabo de la siguiente manera: sort sortId . Si se quiere definir varios tipos de golpe, sorts sortId1, sortId2, … , Nótese la importancia de que todas las instrucciones de un programa escrito en Maude acaben en un punto precedido por un espacio, Para establecer una jerarquía entre los tipos se definen los subtipos a no declarar ciclos en la jerarquía subsort sortId1 < sortId2 . subsort sortId2 < sortId3 . O bien: subsorts sortId1 < sortId2 < sortId3 . 1.3.3. Operadores La sintaxis para declarar operadores es la siguiente: op opId : sortId1 sortId2 … sortIdX [operator attributes] . Si varios operadores comparten los mismos tipos, se declaran de la siguiente forma: ops opId1 opId2: sortId1 sortId2 … sortOperator . 1.3.4. Variables Se pueden declarar instancias de los tipos definidos para un sistema, para así poder d ecuaciones y reglas. Las variables se declaran de la siguiente forma: var N : tipoN . Si son varias variables del mismo tipo vars N M : tipoN . Lo primero que se necesita definir en un sistema son los tipos. La definición de tipos definir varios tipos de golpe, se puede utilizar la palabra sorts : sorts sortId1, sortId2, … , sortIdX . que todas las instrucciones de un programa escrito en Maude acaben en un punto precedido por un espacio, pues de lo contrario la compilación fallaría. Para establecer una jerarquía entre los tipos se definen los subtipos . Hay que prestar la jerarquía . subsort sortId1 < sortId2 . subsort sortId2 < sortId3 . subsorts sortId1 < sortId2 < sortId3 . La sintaxis para declarar operadores es la siguiente: sortId1 sortId2 … sortIdX -> [operator attributes] . Si varios operadores comparten los mismos tipos, se declaran de la siguiente forma: ops opId1 opId2: sortId1 sortId2 … sortIdX declarar instancias de los tipos definidos para un sistema, para así poder d Las variables se declaran de la siguiente forma: varias variables del mismo tipo : N M : tipoN . 17 La definición de tipos se lleva a que todas las instrucciones de un programa escrito en Maude acaben de lo contrario la compilación fallaría. Hay que prestar atención sortOperator Si varios operadores comparten los mismos tipos, se declaran de la siguiente forma: sortIdX -> declarar instancias de los tipos definidos para un sistema, para así poder d efinir sus 1.3.5. Ecuaciones no condicio Las ecuaciones se declaran mediante la palabra reservada eq termino1 = termino2 [atributos] T ambién existen las ecuaciones condicionales, pero no 1.3.6. Reglas Las reglas son un instrumento para la siguiente: rl [etiqueta] : término1 => término2 [atributos] Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que si se encuentra una instancia de la parte izqui será reemplazado por la parte posibilidad de que la ejecución de varias reglas sea concurrente. Las reglas también pueden ser condicionales. condicio nales Las ecuaciones se declaran mediante la palabra reservada eq de la siguiente manera: termino1 = termino2 [atributos] ambién existen las ecuaciones condicionales, pero no se usarán en este programa. Las reglas son un instrumento para la reescrit ura en Maude. La sintaxis para é [etiqueta] : término1 => término2 [atributos] Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que si se encuentra una instancia de la parte izqui erda en el estado actual, en el estado siguiente parte derecha de la regla. Lo más potente de e ste concepto es la posibilidad de que la ejecución de varias reglas sea concurrente. Las reglas también pueden ser condicionales. 18 de la siguiente manera: programa. ura en Maude. La sintaxis para é stas es la Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que erda en el estado actual, en el estado siguiente ste concepto es la En esta sección se presentan primera versión donde los operadores adicionales de la lógica temporal se declaran en función de los operadores básicos y los operadores adicionales sin tener que pasar por la conversión a los la primera se explican todos los elementos declarados, parte del código es parecida , así que 2.1. Versión simple La implementación está estructurada en d módulo de sistema TEMPLOGIC 2.1.1. Módulo funcional En el módulo TEMPLOGIC , se van a y ecuaciones. fmod TEMPLOGIC is protecting BOOL . protecting QID . TEMPLOGIC importa el módulo expresar el valor de verdad d utilizar el tipo Qid y así utilizar cualquier cadena de caracteres como una variable a la hora de hacer pruebas 2.1.2. Tipos Los tipos básicos de TEMPLOGIC  Prop: el tipo de las proposiciones  Fórmula: el tipo para representar  Literal: representa una proposición lógica o  LiNext: fórmula compuesta por  SetLiteral: conjunto de literales  SetLiNext: conjunto de literales y/o expresiones  SetFormula: conjunto de  NESetFormula: conjunto y para considerar casos en lo  History: historial de un nodo.  Estado: indica la fase de  Nodo: el elemento nodo e entre corchetes, y finalmente  SetNodos: e xpresa la disyunc “punto y coma”. Los tipos anteriores pueden clasifi del árbol: Nodo , SetFormula que c onstruyen la fórmula PLTL 2. Imp lementación y análisis se presentan dos versiones de la implementació n del algoritmo Tableau donde los operadores adicionales de la lógica temporal se declaran en función y una versión extendida donde se declaran reglas de Tableau para los operadores adicionales sin tener que pasar por la conversión a los operadores todos los elementos declarados, mientras que para la se , así que sólo se comentan las diferencias con la primera versión La implementación está estructurada en d os módulos : El módulo funcional LOGIC -RULES . , se van a definir los tipos del programa, su jerarquía, sus protecting BOOL . protecting QID . importa el módulo BOOL , ya que el tipo de datos booleano es necesario expresar el valor de verdad d e las fórmulas. También se importa el módulo así utilizar cualquier cadena de caracteres precedida por el carácter a la hora de hacer pruebas . TEMPLOGIC son: las proposiciones lógicas. para representar fórmulas lógicas una proposición lógica o su negación (p o ¬p). fórmula compuesta por un literal y/o una expresión Next de literales de literales y/o expresiones Next de fórmulas, que estarán separadas por comas. conjunto de fórmulas no nulas. Éste tipo se crea para poder declarar el id, casos en lo s que se necesita que la SetFormula no esté vacía historial de un nodo. Es necesario para la detección de bucles. comprobación en la que se encuentra el algoritmo. nodo e ngloba el estado actual, seguido de la fórmula y finalmente el separador D() que contendrá la fórmula distinguida. xpresa la disyunc ión entre los nodos del árbol. Éstos están Los tipos anteriores pueden clasifi carse en dos clases: los ti pos que se refieren SetFormula , SetLiNext , SetLiteral , History y SetNodos onstruyen la fórmula PLTL : Formula , Prop , Literal , LiNext y Next . 19 lementación y análisis n del algoritmo Tableau : Una donde los operadores adicionales de la lógica temporal se declaran en función donde se declaran reglas de Tableau para operadores básicos; para para la se gunda gran primera versión . : El módulo funcional TEMPLOGIC y el definir los tipos del programa, su jerarquía, sus operadores es necesario para el módulo QID para poder precedida por el carácter “ ‘ “ para poder declarar el id, esté vacía . se encuentra el algoritmo. fórmula y su historial que contendrá la fórmula distinguida. separados por un pos que se refieren a la estructura SetNodos , y los tipos La jerarquía de tipos está pensada de forma que los tipos referentes a la estructura del árbol serán manipulados de forma separada codificar las ecuaciones, no Además, el flujo de ejecución está orientado SetFormula y SetNodos , y nunca al revés, e se verá más adelante. El tipo History se ha declarado como éste, ya que se construye combinando operador “ < ”. La declaración del tipo eventualidad este tipo serán reconocidas mediante el operador A continuación, se presenta el código Maude donde se declaran sorts Prop Literal Next LiNext Formula . sorts SetLiteral SetLiNext NESetFormula SetFormula . subsort Qid < Pr op subsort Bool < Pr op subsort Prop < Literal < LiNext < Formula . subsort Next < LiNext . subsort Literal < SetLiteral . subsort LiNext < SetLiNext . subsort Formula < NESetFormula < SetFormula . subsort SetLiteral < SetLiNext < NESetFormula . sort History . subsort Se tFormula < History . sorts Nodo SetNodos . subsort Nodo < SetNodos . sort Estado . A continuación se muestra un gráfico con la jerarquía de los tipos clases de tipos mencionadas anteriormente La jerarquía de tipos está pensada de forma que los tipos referentes a la estructura del árbol serán manipulados de forma separada a los del interior de la fórmula lógica. A se permite que dentro de una fórmula haya el flujo de ejecución está orientado a convertir los operadores de las fórmula , y nunca al revés, e xcepto en el caso de la función se ha declarado como supertipo de SetFormula y de todos los subtipos de ya que se construye combinando varios elementos SetFormula separados por tipo eventualidad puede parecer necesaria, sin embargo las expresiones de mediante el operador Until y sus operandos. A continuación, se presenta el código Maude donde se declaran los tipos. Literal Next LiNext Formula . SetLiteral SetLiNext NESetFormula SetFormula . op . op . < Literal < LiNext < Formula . Next < LiNext . Literal < SetLiteral . LiNext < SetLiNext . Formula < NESetFormula < SetFormula . SetLiteral < SetLiNext < NESetFormula . tFormula < History . Nodo SetNodos . Nodo < SetNodos . un gráfico con la jerarquía de los tipos recién comentados clases de tipos mencionadas anteriormente están separadas en diferentes columnas. 20 La jerarquía de tipos está pensada de forma que los tipos referentes a la estructura del árbol a los del interior de la fórmula lógica. A la hora de haya un SetFormula . los operadores de las fórmula s en xcepto en el caso de la función toFormula que y de todos los subtipos de separados por el sin embargo las expresiones de recién comentados . Las dos separadas en diferentes columnas. 2.1.3. Operadores Operadores básicos Existen cuatro operadores de base. Por razones técnicas y prácticas, se les representa de otra forma en Maude, como figura Tabla 7: Representaciones de los operadores básicos Se declaran tres operadores not el tipo Prop . De esta forma se construye op ^_ : Formula op ^_ : Next op ^_ : Prop El operador X se aplica sobre una fórmula, y produce una fórmula de tipo op X_ : Formula Nombre Símbolo Not ¬ And ∧ Next X Until U Figura 2: Jerarquía de los tipos operadores de base. Por razones técnicas y prácticas, se les representa de otra figura en la siguiente tabla. de los operadores básicos not : uno para el tipo Formula , otro para el tipo De esta forma se construye el tipo literal y el tipo LiNext . ^_ : Formula -> Formula . ^_ : Next -> LiNext . -> Literal . se aplica sobre una fórmula, y produce una fórmula de tipo Next X_ : Formula -> Next . Operador en Maude ^ /\ X U 21 operadores de base. Por razones técnicas y prácticas, se les representa de otra el tipo Next y otro para Next . Los operadores And y U se aplican sobre tipo. op _/\ _ : Formula Formula op _U_ : Formula Formula En Maude es posible declarar los atributos de asociatividad y conmutatividad sin tener que definir ecuaciones específicas (And) no necesita las propiedades transformará en el operador para evitar que aparezcan avisos de ambigüedad, como por ejemplo: Warning: <standard input>, line 177: am [(('p U 'q) /\ (^ X F 'q / -versus- [((('p U 'q) /\ ^ X F 'q) / Arbitrarily taking the first as correct. Operadores adicionales A continuación se declaran los operadores adicionales. El operador \/ (Or) posee los atributos de asociatividad y conmut que el operador /\. Este se convertirá posteriormente en el operador op _\ /_ : Formula Formula Los operadores R , F y G reciben y devuelven el tipo op _R_ : Formula Formula op G_ : Formula op F_ : Formula El operador T (then) representa la implicación l a fase de testeo ya que las pruebas utilizadas contienen este operador. op _T_ : Formula Formula Operador “coma” El operador coma puede concatenar fórmulas, literales o fórmulas de tipo asociativo y conmutativo, y tendrá como id op nil : op _,_ : SetFormula SetFormula op _,_ : SetLiNext SetLiNext op _,_ : SetLiteral SetLiteral La declaración del id para el operador coma es importante. Implica que un utilizado en una ecuación puede diferente para cada uno de los La siguiente declaración del operador coma es necesaria p correctamente. Sin esta declaración, se haría matching de forma indefinida con el elemento nil , y la ejecución no terminaría. La solución consiste en forzar que que el de cualquier fórmula SetFormula. se aplican sobre el tipo formula y dan como resultado el mismo _ : Formula Formula -> Formula [comm assoc] . _U_ : Formula Formula -> Formula . En Maude es posible declarar los atributos de asociatividad y conmutatividad sin tener que específicas para ello (ver ejemplo anterior). Técnicamente, e las propiedades de asociatividad y conmutatividad ya que coma, y és te sí las tiene. Sin embargo, añadimos estos atributos para evitar que aparezcan avisos de ambigüedad, como por ejemplo: Warning: <standard input>, line 177: am biguous term, two parses are: (^ X F 'q / \ ^ 'q)) < noH]D(noD) ^ X F 'q) / \ ^ 'q) < noH]D(noD) Arbitrarily taking the first as correct. se declaran los operadores adicionales. posee los atributos de asociatividad y conmut atividad por la misma razón Este se convertirá posteriormente en el operador “ punto coma /_ : Formula Formula -> Formula [comm assoc] . reciben y devuelven el tipo Formula . _R_ : Formula Formula -> Formula . G_ : Formula -> Formula . F_ : Formula -> Formula . representa la implicación y se declara por razones técnicas. Será útil para a fase de testeo ya que las pruebas utilizadas contienen este operador. _T_ : Formula Formula -> Formula . coma puede concatenar fórmulas, literales o fórmulas de tipo asociativo y conmutativo, y tendrá como id el operador nil. nil : -> SetFormula . _,_ : SetFormula SetFormula -> SetFormula [comm assoc id: nil] . : SetLiNext SetLiNext -> SetLiNext [comm assoc id: nil] . _,_ : SetLiteral SetLiteral -> SetLiteral [comm assoc id: nil] . La declaración del id para el operador coma es importante. Implica que un utilizado en una ecuación puede ser nulo, y esto evita tener que escribir cada uno de los casos. del operador coma es necesaria p ara que el atributo Sin esta declaración, se haría matching de forma indefinida con el elemento , y la ejecución no terminaría. La solución consiste en forzar que nil sea de tipo cualquier fórmula . Se usa el tipo NESetFormula ya que es un subtipo del tipo 22 y dan como resultado el mismo En Maude es posible declarar los atributos de asociatividad y conmutatividad sin tener que Técnicamente, e l operador /\ ya que en el futuro se te sí las tiene. Sin embargo, añadimos estos atributos biguous term, two parses are: atividad por la misma razón punto coma ”. se declara por razones técnicas. Será útil para coma puede concatenar fórmulas, literales o fórmulas de tipo LiNext. Será id: nil] . id: nil] . id: nil] . La declaración del id para el operador coma es importante. Implica que un SetFormula S escribir una ecuación ara que el atributo id funcione Sin esta declaración, se haría matching de forma indefinida con el elemento sea de tipo mayor es un subtipo del tipo op _,_ : SetFormula NESetFormula Operadores cons tructores del nodo El operador < perm ite ordenar el más recientes ), lo cual permite propiedad asociativa, pero no la conmutativa ya que el orden es significativo. op _<_ : History History El operador noH indica que no hay historial, op noH : La ejecución de las ecuaciones en Maude es no determinista, lo cual significa que no se puede asegurar que se ejecute n en un orden punto 3.3). Para asegurar que estado: cada esta do representa una fase anterior. Técnicamente, se declara el é ste. Se dispondrá de 7 estados: paso del algoritmo de Tableau, S1 se corresponde con el paso 2 del mismo, S2 con el paso, S4 con el quinto, S5 con el cuarto, y correspondencia entre los estados S4 y S5 con las fases del algoritmo es un detalle técnico de la implementación y no cambia el resultado de la ejecución. Las ecuaciones Tableau usarán estos operad y si se hace un matching se pasará al estado siguiente del algoritmo. ops S0 S1 S2 S3 S4 S5 SF : Los operadores T0 y T1 representan transiciones entre los estados. declaran en el módulo de sistema del programa. técnicamente resulta útil para saber la regla que se está aplicando y por lo tanto la fase actual del algoritmo. ops T0 T1 : Nótese que las transiciones se realizan para las comprobaciones que resultan ciertas y reescriben la fórmula. Esto solo ocurre para los estados S0 y S1. Para el resto de estados, no se declaran transicio nes, ni tampoco para el nodo final. La repre sentación del nodo requiere simplicidad Primero se guarda el estado actual del algoritmo, seguido actual , envueltos entre corchetes, y A continuación, se muestra la d op _[_] D( _) : Estado History Formula El hecho de envolver el historial del nodo e hora de escribir las ecuaciones. asegura que no haya reescrituras en _,_ : SetFormula NESetFormula -> NESetFormula[comm assoc tructores del nodo ite ordenar el historial por antigüedad (las fórmulas se guardan de menos ), lo cual permite localizar fácilmente la fórmula actual del nodo. Posee la propiedad asociativa, pero no la conmutativa ya que el orden es significativo. _<_ : History History -> History [assoc] . indica que no hay historial, esto ocurre en el caso del nodo inicial. noH : -> History . La ejecución de las ecuaciones en Maude es no determinista, lo cual significa que no se puede n en un orden dado (esto se explica de forma más detallada en el asegurar que el algoritmo sigue el orden esperado se usa el concepto de do representa una fase de comprobación del algoritmo visto en la sección tipo estado, y a continuación un operador por cada instancia de ste. Se dispondrá de 7 estados: S0 representa la fase inicial y se corresponde con el primer paso del algoritmo de Tableau, S1 se corresponde con el paso 2 del mismo, S2 con el paso, S4 con el quinto, S5 con el cuarto, y SF es la fase final. El cambio de orden en la correspondencia entre los estados S4 y S5 con las fases del algoritmo es un detalle técnico de y no cambia el resultado de la ejecución. ecuaciones Tableau usarán estos operad ores para saber en qué fase del algoritmo se está, se pasará al estado siguiente del algoritmo. ops S0 S1 S2 S3 S4 S5 SF : -> Estado . representan transiciones entre los estados. Estas declaran en el módulo de sistema del programa. Su uso no es imprescindible, sin embargo, técnicamente resulta útil para saber la regla que se está aplicando y por lo tanto la fase actual ops T0 T1 : -> Estado . Nótese que las transiciones se realizan para las comprobaciones que resultan ciertas y reescriben la fórmula. Esto solo ocurre para los estados S0 y S1. Para el resto de estados, no se nes, ni tampoco para el nodo final. sentación del nodo requiere simplicidad , a pesar de contener mucha información. el estado actual del algoritmo, seguido del historial que incluye la fórmula , envueltos entre corchetes, y por último la fórmula distinguida. la d eclaración del operador nodo: _) : Estado History Formula -> Nodo . el historial del nodo e ntre corchetes permite manejarlo fácilmente a la las ecuaciones. L as ecuaciones aplican la reescritura al nodo entero reescrituras en el interior del historial. 23 assoc id: nil] . (las fórmulas se guardan de menos a actual del nodo. Posee la del nodo inicial. La ejecución de las ecuaciones en Maude es no determinista, lo cual significa que no se puede (esto se explica de forma más detallada en el se usa el concepto de de comprobación del algoritmo visto en la sección operador por cada instancia de y se corresponde con el primer paso del algoritmo de Tableau, S1 se corresponde con el paso 2 del mismo, S2 con el tercer El cambio de orden en la correspondencia entre los estados S4 y S5 con las fases del algoritmo es un detalle técnico de algoritmo se está, Estas transiciones se uso no es imprescindible, sin embargo, técnicamente resulta útil para saber la regla que se está aplicando y por lo tanto la fase actual Nótese que las transiciones se realizan para las comprobaciones que resultan ciertas y reescriben la fórmula. Esto solo ocurre para los estados S0 y S1. Para el resto de estados, no se , a pesar de contener mucha información. del historial que incluye la fórmula manejarlo fácilmente a la as ecuaciones aplican la reescritura al nodo entero , así se La fórmula distinguida está contenida dentro del algoritmo se ha visto que esta fórmula solo puede ser q ) . Sin embargo, también se pueden distinguir eventualidades a las que se aplica el operador X y para facilitar la distinción entre ambos ca la fórmula distinguida será Formula cada estado del nodo. El operador noD se utiliza para indicar que no hay expresión distinguida en el op noD : - > Formula . Operador “punto coma” op _;_ : SetNodos SetNodos El operador punto coma representa la disyunción entre nodos o grupos d de Tableau. Es conmutativo por porque se utilizan paréntesis y de esta manera se conserva 2.1.4. Ecuaciones Primero se declaran las variables para su posterior uso vars h h1 h2 : History . vars s t : SetFormula . vars nes : NESetFormula . vars f g d : Formula . vars sl : SetLiteral . vars sln : SetLiNext . Las primeras e cuaciones por definir serán función de los básicos. eq true = ^ false . eq e \ / f = ^(^ e / eq G(e) = ^ F(^ e) . eq F(e) = true U e . eq e R f = ^ (^ e U ^ f) . eq e T f = ^ (e / \ A continuación, se exponen las ecuaciones que Se presentan por separado l as ecuacion Fase 0 El primer paso del algoritmo Tableau contradicción. Si el caso se da false , y borrando la fórmula distinguida si la hay. De lo contrario se pasa a la fase 1 eq S0[(s, false) < h] D(d) = SF[ eq S0[(s, f,^ f) < h] D(d) = SF[ [owise]. eq S0[h] D(d) = S1[h] D(d) [ Fase 1 Si el estado actual es S1, s e comprueba un nodo final abierto. Si no , La fórmula distinguida está contenida dentro del separador D() . En la explicación del algoritmo se ha visto que esta fórmula solo puede ser una eventualidad (fórmula . Sin embargo, también se pueden distinguir eventualidades a las que se aplica el operador y para facilitar la distinción entre ambos ca sos se guardará la fórmula de tipo Formula . Nótese que solo puede haber una fórmula distinguida en para indicar que no hay expresión distinguida en el > Formula . _;_ : SetNodos SetNodos -> SetNodos [comm] . El operador punto coma representa la disyunción entre nodos o grupos d e nodos Es conmutativo por que el orden no es importante, e n cambio no paréntesis y de esta manera se conserva la profundidad de cada Primero se declaran las variables para su posterior uso en las ecuaciones. h h1 h2 : History . s t : SetFormula . nes : NESetFormula . f g d : Formula . sl : SetLiteral . sln : SetLiNext . cuaciones por definir serán aquéllas que expresan los operadores adicionales en true = ^ false . / f = ^(^ e / \ ^ f) . G(e) = ^ F(^ e) . F(e) = true U e . e R f = ^ (^ e U ^ f) . \ ^ f) . las ecuaciones que implementan las comprobaciones de Tableau. as ecuacion es de cada fase del algoritmo. El primer paso del algoritmo Tableau consiste en ver si la fórmula contiene el caso se da , se pasa a la fase final, d ando como resultado fórmula distinguida si la hay. fase 1 (S1). < h] D(d) = SF[ false < (s, false) < h] D(noD) . S0[(s, f,^ f) < h] D(d) = SF[ false < (s, f, ^ f) < h] S0[h] D(d) = S1[h] D(d) [ owise] . e comprueba si la fórmula actual es igual a true , si es así , se simplifica la fórmula, p or ejemplo eliminando 24 En la explicación del una eventualidad (fórmula de forma p U . Sin embargo, también se pueden distinguir eventualidades a las que se aplica el operador sos se guardará la fórmula de tipo Next . El tipo de puede haber una fórmula distinguida en para indicar que no hay expresión distinguida en el nodo. e nodos en el árbol n cambio no es asociativo la profundidad de cada subárbol. que expresan los operadores adicionales en las comprobaciones de Tableau. contiene false o una ando como resultado la proposición < h] D(noD) . < (s, f, ^ f) < h] D(noD) si es así se obtiene or ejemplo eliminando las constantes true o las proposiciones repetidas ( NESetFormula ). Se repite el proceso ha momento en que se pasará a la fase 2 eq S1[(^ false ) < h] D(d eq S1[(nes, ^ false eq S1[(nes, f, f) < h] eq S1[h] D(d) = S2[h] D(d) [ Fase 2 Si el estado actual es S2, s e verifica ( sl es una variable de tipo SetLiteral nodo es abierto. En caso contr eq S2[sl < h] D(d) = SF[^ eq S2[h] D(d) = S3[h] D(d) [ Fase 3 En el estado S3 se verifica s i existen bucles en el árbol algún punto del historial que no sea el actual, comprobar que en caso de que el historial cumplan . En caso afirmativo el nodo final resultante será En otro caso se pasa a la fase 4 eq S3[s < h2 < s < h1] SF[loopIsTrue(s < h2) < s < h2 < s < h1] D(noD) . eq S3[h] D(d) = S4[h] Fase 4 S e comprueba si la fórmula es una colección de fórmulas invocan las funciones next funciones se encargan de realizar el paso en el tiempo para la fórmula distinguida respectivamente comprobaciones. Si la fórmula actual no es de tipo eq S4[sln < h]D(d) = T0[next(sln) < sln < h] D(nextD(d)) . eq S4[h] D(d) = S5[h] D(d) [ Fase 5 En la fase 5 se ejecutan las ecuaciones T En el siguiente bloque de código se realiza la operación negación se convierte en afirmación, y se retorna a la fase comprobaciones. eq S5[(s, ^ ^ f) < h] D(d) = proposiciones repetidas ( nótese que se usa l a variable ). Se repite el proceso ha sta que la fórmula actual ya no a la fase 2 (S2). ) < h] D(d ) = SF[(^ false) < h] D(noD) . false ) < h] D(d) = T1[nes < (nes, ^ false ) < h] D(d) . S1[(nes, f, f) < h] D(d) = T1[(nes, f) < (nes, f, f)< h] S1[h] D(d) = S2[h] D(d) [ owise] . e verifica si la fórmula hace matching con una colección de literales SetLiteral ). Si es el caso, se transita a un estado En caso contr ario se va al estado S3 . S2[sl < h] D(d) = SF[^ false < sl < h] D(d) . S2[h] D(d) = S3[h] D(d) [ owise] . i existen bucles en el árbol . Si la fórmula actual s que no sea el actual, se invoca la función loopIsTrue que en caso de que el historial contenga eventualidades, las premi . En caso afirmativo el nodo final resultante será abierto , de lo contrario será la fase 4 . S3[s < h2 < s < h1] D(d) = SF[loopIsTrue(s < h2) < s < h2 < s < h1] D(noD) . S4[h] D(d) [owise] . e comprueba si la fórmula es una colección de fórmulas de tipo LiNext . Si y nextD (que serán explicadas en el apartado 3.1.5 realizar el paso en el tiempo para la fórmula actual y la fórmula respectivamente . Seguido, se retorna a la fase inicial para Si la fórmula actual no es de tipo LiNext se pasa a la fase 5. S4[sln < h]D(d) = T0[next(sln) < sln < h] D(nextD(d)) . D(d) = S5[h] D(d) [ owise] . las ecuaciones T ableau de los operadores. En el siguiente bloque de código se realiza la operación de la doble negación negación se convierte en afirmación, y se retorna a la fase inicial para reanudar las S5[(s, ^ ^ f) < h] D(d) = T0[(s, f) < (s, ^ ^ f) < h] D(d) . 25 a variable nes de tipo la fórmula actual ya no sea simplificable, ) < h] D(d) . = T1[(nes, f) < (nes, f, f)< h] D(d) [owise] . una colección de literales estado final donde el s se encuentra en loopIsTrue para contenga eventualidades, las premi sas de estas se , de lo contrario será cerrado. . Si es el caso, se en el apartado 3.1.5 ). Estas dos actual y la fórmula inicial para repetir todas las S4[sln < h]D(d) = T0[next(sln) < sln < h] D(nextD(d)) . la doble negación . La doble inicial para reanudar las T0[(s, f) < (s, ^ ^ f) < h] D(d) . 32 3.1. Ejemplo ilustrativo En esta sección se presenta extendida de la implementación explicarán los elementos más importantes Para hacer pruebas, se p uede frewrite o search . En el anexo de este documento se puede encontrar información sobre funcionamiento de cada uno de ellos Para elegir uno de los tres comandos anteriores, hay que tener en cuenta que el programa implementado impone un orden secuencia sea cual sea el comando elegido El comando rewrite será el que se us arriba-abajo (top down ) y ejecuta las reglas no es el mejor comando posible pero en el caso actual resulta solución, y no existe e l riesgo de que la ejecución no termine Generalmente, el comando search asegura que se va a llegar a una solución. a apreciar , y el resultado será i Las ventajas del comando frewrite caso actual. É ste utiliza una estrategia justa en cuanto a la aplicación de las reglas, de forma que no habrá reglas que nunca se utilidad ya que el algoritmo actual impone un orden para la ejecución de las reglas. Se d ispone de una opción para comando siguiente. set trace on . Se emplea el comando rewrite es S0 y por lo tanto el historial distinguida ( noD) . rewrite in TEMPLOGIC A continuación se muestra una parte de la traza de la ejecución: eq S5[(s:SetFormula,f:Formula / f:Formula,g:Formula) < (s:SetFormula,f:Formula / s:SetFormula -- > nil f:Formula -- > 'p U 'q g:Formula -- > ^ 'q h --> noH d --> noD S5[(^ 'q /\ ('p U 'q)) < noH]D(noD) 3. Pruebas y ilustrativo un ejemplo simple de la ejecución del programa extendida de la implementación . Para ello se usará la fórmula (p U q ) los elementos más importantes para interpretar el resultado. uede usar cualquiera de los tre s comandos de Maude En el anexo de este documento se puede encontrar información sobre cada uno de ellos . Para elegir uno de los tres comandos anteriores, hay que tener en cuenta que el programa impone un orden secuencia l en la ejecución de las ecuaciones, esto hace que sea cual sea el comando elegido , el resultado será el mismo. será el que se us ará para realizar las pruebas. É ste utiliza una estrategia ) y ejecuta las reglas desde el exterior (outermost). En casos posible , ya que existen posibilidades de que la ejecución no termine, resulta ser el más simple y rápido en cuanto a la búsqueda de l riesgo de que la ejecución no termine . search suele ser el más recomendado , ya que es el único que asegura que se va a llegar a una solución. Sin embargo, esta ventaja en el caso actual no se va , y el resultado será i gual que utilizando el rewrite . frewrite frente al rewrite también resultan invisibles en el ste utiliza una estrategia justa en cuanto a la aplicación de las reglas, de forma que no habrá reglas que nunca se consideren . Como ya se mencionó, esto no tendrá ninguna utilidad ya que el algoritmo actual impone un orden para la ejecución de las reglas. ispone de una opción para visualizar la traza de la ejecución . Para ello se deb rewrite para validar la fórmula (p U q) /\ ^ q . el historial es vacio ( noH) , y tampoco se dispone de un LOGIC -RULES : S0[(^ 'q /\ ('p U 'q)) < noH]D(noD) . una parte de la traza de la ejecución: eq S5[(s:SetFormula,f:Formula / \ g:Formula) < h]D(d) = T0[(s:SetFormula, f:Formula,g:Formula) < (s:SetFormula,f:Formula / \ g:Formula) < h]D(d) . > nil > 'p U 'q > ^ 'q ('p U 'q)) < noH]D(noD) 33 y resultados programa usando la regla ) /\ ¬ q, y se s comandos de Maude rewrite , En el anexo de este documento se puede encontrar información sobre el Para elegir uno de los tres comandos anteriores, hay que tener en cuenta que el programa en la ejecución de las ecuaciones, esto hace que ste utiliza una estrategia En casos generales, ya que existen posibilidades de que la ejecución no termine, ser el más simple y rápido en cuanto a la búsqueda de la , ya que es el único que esta ventaja en el caso actual no se va también resultan invisibles en el ste utiliza una estrategia justa en cuanto a la aplicación de las reglas, de forma . Como ya se mencionó, esto no tendrá ninguna utilidad ya que el algoritmo actual impone un orden para la ejecución de las reglas. . Para ello se deb e invocar el . El estado actual tampoco se dispone de un a fórmula 'q)) < noH]D(noD) . g:Formula) < h]D(d) = T0[(s:SetFormula, g:Formula) < h]D(d) . ---> T0[(nil,('p U 'q),^ 'q) < (^ 'q / En las dos primeras líneas comprobaciones de las fases considerados por éstas) . A continuación se presentan encontradas en la fórmula inicial dos últimas líneas representan En este paso se está aplicando la ecuación coma. El resultado final de la evaluación de la fórmula rewrite in TEMPLOGIC SF[^ false < noH]D(noD) rewrites: 48 in 1628036047000ms cpu (202ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) El resultado indica que la fórmula reescrituras ( incluyendo ecuaciones y reglas reales. Debe tenerse en cuenta que cuando la ejecución aumenta. Finalmente se ve el tipo del r esultado que es Si se quisiera visualizar el historial que simplifican el árbol y eliminan el historial rewrites: 53 in 16280360470 result SetNodos: (SF[^ false < 'q < (('p / < ('p,^ 'q,X (('p / < ('p,^ 'q,^ 'q,X (('p / < (^ 'q / SF[false < ('p,^ 'q,^ ^ 'q,X (false U < (^ 'q,X (false U 'q),'p / < ('p,^ 'q,X (('p / < ('p,^ 'q,^ 'q,X (('p / < (^ 'q / SF[false < ('q,^ 'q) < (^ 'q,('p U 'q)) < (^ 'q / Con este resultado se observa fórmula, y dos nodos cerrado 3.2. Pruebas 3.2.1. Pruebas unitarias Se han realizado pruebas unitarias totalidad de los casos. Son 157 Como ejemplo, se muestran de cada prueba aparecen los resultados esperados. T0[(nil,('p U 'q),^ 'q) < (^ 'q / \ ('p U 'q)) < noH]D(noD) aparece la ecuación que se va a aplicar ( se han de las fases anteriores a la fase 5 ya que no se cumplen los casos . A continuación se presentan todas las instancias para las variables inicial que permiten la aplicación de la ecuación dos últimas líneas representan la fórmula antes y después de aplicar la ecuación. se está aplicando la ecuación and para convertir el operador / \ de la evaluación de la fórmula es el siguiente: LOGIC -RULES : S0[(^ 'q /\ ('p U 'q)) < noH]D(noD) . SF[^ false < noH]D(noD) rewrites: 48 in 1628036047000ms cpu (202ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) la fórmula (p U q) /\ ^ q es cierta. S e incluyendo ecuaciones y reglas ) y el tiempo de ejecución es de en cuenta que cuando la visualización de la traza está activa el tiempo de esultado que es Nodo seguido del árbol resultante el historial y el árbol entero habría que comentar las líneas de código que simplifican el árbol y eliminan el historial , y se obtendría lo siguiente: rewrites: 53 in 16280360470 00ms cpu (245ms real) (0 rewrites/second) (SF[^ false < 'q < (('p / \ ^ ^ 'q) U 'q) < ('p,^ 'q,X (('p / \ ^ ^ 'q) U 'q)) < ('p,^ 'q,^ 'q,X (('p / \ ^ ^ 'q) U 'q)) < (^ 'q,('p U 'q)) (^ 'q / \ ('p U 'q)) < noH]D(noD) ; SF[false < ('p,^ 'q,^ ^ 'q,X (false U 'q)) < (^ 'q,X (false U 'q),'p / \ ^ ^ 'q) < (('p /\ ^ ^ 'q) U 'q) 'q,X (('p / \ ^ ^ 'q) U 'q)) < ('p,^ 'q,^ 'q,X (('p / \ ^ ^ 'q) U 'q)) < (^ 'q, < (^ 'q / \ ('p U 'q)) < noH]D(noD)) ; SF[false < ('q,^ 'q) < (^ 'q,('p U 'q)) < (^ 'q / \ ('p U 'q)) < noH]D(noD) observa que existe un nodo abierto y por lo tanto un modelo cerrado s. unitarias para todos los operadores y funciones, intentando cubrir 157 las pruebas que se han escrito. las pruebas que se hicieron para la función loopIsTrue de cada prueba aparecen los resultados esperados. 34 ('p U 'q)) < noH]D(noD) se han ignorado las ya que no se cumplen los casos instancias para las variables que permiten la aplicación de la ecuación , y finalmente las fórmula antes y después de aplicar la ecuación. \ en el operador ('p U 'q)) < noH]D(noD) . rewrites: 48 in 1628036047000ms cpu (202ms real) (0 rewrites/second) e han realizado 48 el tiempo de ejecución es de 202 milisegundos traza está activa el tiempo de árbol resultante . habría que comentar las líneas de código 00ms cpu (245ms real) (0 rewrites/second) ^ ^ 'q) U 'q)) < (^ 'q,('p U 'q)) ^ ^ 'q) U 'q) 'q, ('p U 'q)) nodo abierto y por lo tanto un modelo para la intentando cubrir la loopIsTrue . Al lado rew loopIsTrue(noH) rew loopIsTrue( 'p rew loopIsTrue(( 'p rew loopIsTrue(( 'p rew loopIsTrue((( 'p rew loopIsTrue((( 'p rew loopIsTrue(( 'p rew loopIsTrue(( 'p El resto d e pruebas unitarias se adjunta 3.2.2. Pruebas globales En este punto se m uestran funcionamiento del al goritmo. (3). Se utilizará la versión extendida para las pruebas Maude así como el árbol que lo represent Ejemplo 1: Evaluación de la fórmula rewrite in TEMPLOGIC rewrites: 98 in 1628036047000ms cpu (4ms real) result Nodo: SF[^ false < noH]D(noD) A continuación se detalla n los pasos más importantes fórmula F ^ 'q /\ ('p U 'q) Primero se aplica la regla Seguidamente se distingue la fórmula crean dos nodos, y se distingue la eventualidad En el paso siguiente, al ser la eventualidad distinguida diferente de la se aplica la regla until dando lugar a dos ramas. fórmulas ^ q y ^^ q y por lo t rama izquierda se simplifica (se elimina la fórmula repetida operador X para pasar a un nuevo instante de tiempo. El resultado obtenido son cuatro hojas cerradas y dos abiertas y por lo tanto la fórmula /\ (p U q) es válida. Las dos hojas abiertas represe modelo sería: E(S 0 ) = {p = true, q = false} , E El segundo modelo sería: E(S 0 ) = {q = true} , E(S 1 ) = {q = false} rew loopIsTrue(noH) . *** ^ false 'p < noH) . *** ^ false 'p U 'q) < 'p < noH) . *** false 'p U 'q) < 'q < noH) . *** ^ false 'p U 'q), 'q) < 'p < noH) . *** ^ false 'p U 'q), 'q) < 'q < noH) . *** ^ false 'p U 'q) < ('p U 'q) < 'q < noH) . *** ^ false 'p U 'q) < ('p U 'q) < 'p < noH) . *** false e pruebas unitarias se adjunta en el anexo de este documento. uestran los principales ejemplos utilizad os para verificar el buen goritmo. Los cinco ejemplos fuero n extraídos de los documentos extendida para las pruebas , y se expondrán los resul tados Maude así como el árbol que lo represent a, para mayor claridad. de la fórmula F ^ 'q /\ ('p U 'q) LOGIC -RULES : S0[(F ^ 'q /\ ('p U 'q)) < noH]D(noD) . rewrites: 98 in 1628036047000ms cpu (4ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) n los pasos más importantes de l a aplicación del algoritmo a la ('p U 'q) : Primero se aplica la regla And para convertir el operador /\ en el operador “com Seguidamente se distingue la fórmula p U q y se aplica la regla Until(s ) y se distingue la eventualidad (p /\ ^ F ^ q) U q dentro del operador X. En el paso siguiente, al ser la eventualidad distinguida diferente de la eventualidad actual F ^ q, dando lugar a dos ramas. El nodo de la rama derecha contiene y por lo t anto resulta en un nodo cerrado, mientras que el nodo de la rama izquierda se simplifica (se elimina la fórmula repetida ^ q ) y seguidamente se le aplica el operador X para pasar a un nuevo instante de tiempo. El resultado obtenido son cuatro hojas cerradas y dos abiertas y por lo tanto la fórmula Las dos hojas abiertas represe ntan modelos para la fórmula: El E (S 1 ) = {q = true} ) = {q = false} 35 *** ^ false *** ^ false *** false *** ^ false *** ^ false *** ^ false *** ^ false *** false os para verificar el buen n extraídos de los documentos (1) y tados en código de ('p U 'q)) < noH]D(noD) . (0 rewrites/second) a aplicación del algoritmo a la en el operador “com a”. ) de forma que se dentro del operador X. eventualidad actual F ^ q, El nodo de la rama derecha contiene las anto resulta en un nodo cerrado, mientras que el nodo de la ) y seguidamente se le aplica el El resultado obtenido son cuatro hojas cerradas y dos abiertas y por lo tanto la fórmula F ^ q ntan modelos para la fórmula: El primer Figura Figura 3: Árbol para la fórmula F ^ q /\ (p U q) 36 Ejemplo 2 : Evaluación de la formula p U false Maude> rewrite in TEMP rewrites: 43 in 1628036047000ms cpu (0ms real) (0 rewrites/second) result Nodo: SF[false < noH]D(noD) La evaluación de la fórmula false s e distingue y se aplica la regla ^ false, X(false U false), operador X) resulta de la negación A continuación se aplica la regla del paso en el tiempo obtienen tres nodos con la constante false es falsa. El árbol resultado se muestra a continuación: Ejemplo 3 : Evaluación de la formula Maude> rewrite in TEMP 'q)) < noH]D(noD). : Evaluación de la formula p U false rewrite in TEMP -LOGIC-RULES : S0[('p U false) < noH]D(noD) . rewrites: 43 in 1628036047000ms cpu (0ms real) (0 rewrites/second) result Nodo: SF[false < noH]D(noD) La evaluación de la fórmula p U false ocurre de la siguiente forma: l a eventualidad e distingue y se aplica la regla until(s ). De ello se crean dos nodos: El primero es: ^ false, X(false U false), donde el primer false de la fórmula until la negación del contexto, que al ser vacío, es igual a la constante regla del paso en el tiempo (Next) . Al final de la evaluación se obtienen tres nodos con la constante false , es decir, cerrados, y por lo tanto la fórmula El árbol resultado se muestra a continuación: Figura 4: Árbol para la fórmula p U false : Evaluación de la formula ^ 'q /\ ^ X F 'q /\ ('p U 'q) rewrite in TEMP -LOGIC-RULES : S0[((^ 'q /\ ^ X F 'q) / 'q)) < noH]D(noD). 37 noH]D(noD) . rewrites: 43 in 1628036047000ms cpu (0ms real) (0 rewrites/second) a eventualidad p U De ello se crean dos nodos: El primero es: p, until (dentro del es igual a la constante true . Al final de la evaluación se cerrados, y por lo tanto la fórmula p U ^ X F 'q) / \ ('p U rewrites: 95 in 1628036047000ms cpu (45ms real) (0 result Nodo: SF[false < noH]D(noD) El resultado indica que la fórmula a que existen tres nodos finales cerrados Figura rewrites: 95 in 1628036047000ms cpu (45ms real) (0 rewrites/second) result Nodo: SF[false < noH]D(noD) El resultado indica que la fórmula (^ q) /\ (^ X F q) /\ (p U q) no es válida, debido nodos finales cerrados en el árbol. Figura 5: Árbol para la fórmula (^ q) /\ (^ X F q) /\ (p U q) 38 rewrites/second) no es válida, debido Ejemplo 4 : Evaluación de la fórmula Maude> rewrite in TEMP 'p)) < noH]D(noD) . rewrites: 63 in 1628036047000ms cpu (1ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) Figura : Evaluación de la fórmula 'p /\ X ^ 'p /\ (^ false U ^ 'p) rewrite in TEMP -LOGIC-RULES : S0[('p /\ X ^ 'p / \ 'p)) < noH]D(noD) . rewrites: 63 in 1628036047000ms cpu (1ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) Figura 6: Árbol para la fórmula p /\ X ^ p /\ (^ false U ^ p) 39 \ (^ false U ^ rewrites: 63 in 1628036047000ms cpu (1ms real) (0 rewrites/second) El árbol y la solución obtenid es cierta, ya que se obtienen Ejemplo 5 : Evaluación de la formula Maude> rewrite in TEMP . rewrites: 251 in 1628036047000ms cpu (4ms real) (0 rewrites/second) result Nodo: SF[^ false < La fórmula G F p /\ F ^ q varios bucles. Este ejemplo resulta muy más importantes de la detección de La primera línea contiene la ecuación que detecta el bucle G F 'p . eq S3[s:SetFormula < h2:History < s:SetFormula < h1:History]D(d) = SF[ loopIsTrue (s:SetFormula < h2:History) < s:SetFormula < h2:History < s:SetFormula < h1:History] s:SetFormula -- > G F 'p h2:History -- > ('p,X G F 'p) < X G F 'p,F 'p h1:History -- > ('p,^ 'q,X G F 'p) < ('p,X G F 'p,F ^ 'q) < (X G F 'p,F'p,F ^ 'q) < (G F 'p,F ^ 'q) < (G F 'p / d --> noD ---> SF[loopIsTrue (G F 'p < ('p,X G F 'p) < X G F 'p,F 'p) A continuación se aplica la función premisas de las eventualidades *********** equation eq loopIsTrue (h) = h -- > G F 'p < ('p,X G F 'p) < X G F 'p,F 'p loopIsTrue (G F 'p < ('p,X G F 'p) < X G F 'p,F 'p) ---> promisesAreFulfilled(historyToSetFormula(G F 'p < ('p,X G F 'p) < X G F 'p,F 'p)) En esta parte se comprueba convertido en un SetFormula sustituye por un nodo abierto. *********** equation eq (s:SetFormula,t:SetFormula) contain s:SetFormula -- > ^ false,X G F 'p,X G F 'p,G F 'p,F 'p t:SetFormula -- > 'p y la solución obtenid os indican que la fórmula p /\ X ^ p /\ (^ false U ^ dos nodos cerrados y uno abierto. : Evaluación de la formula G F 'p /\ F ^ 'q rewrite in TEMP -LOGIC-RULES : S0[(G F 'p /\ F ^ 'q) < noH]D(noD) rewrites: 251 in 1628036047000ms cpu (4ms real) (0 rewrites/second) result Nodo: SF[^ false < noH]D(noD) F ^ q resulta válida. Durante la ejecución se detecta Este ejemplo resulta muy largo para exponer, así que se mostrarán importantes de la detección de bucle: la ecuación que detecta el bucle . El nodo repetido es el de la fórmula eq S3[s:SetFormula < h2:History < s:SetFormula < h1:History]D(d) = (s:SetFormula < h2:History) < s:SetFormula < h2:History < s:SetFormula < h1:History] D(noD) . > G F 'p > ('p,X G F 'p) < X G F 'p,F 'p > ('p,^ 'q,X G F 'p) < ('p,X G F 'p,F ^ 'q) < (X G F 'p,F'p,F ^ 'q) < (G F 'p,F ^ 'q) < (G F 'p / \ F ^ 'q) < noH (G F 'p < ('p,X G F 'p) < X G F 'p,F 'p) < G F 'p < (('p,X G F 'p) < X G F 'p,F 'p) < G F 'p < ('p,^ 'q,X G F 'p) < ('p,X G F 'p,F ^ 'q) < (X G F 'p,F 'p,F ^ 'q) < (G F 'p,F ^ ' < (G F 'p /\ F ^ 'q) < noH]D(noD) la función loopIsTrue al bucle para averiguar si se han de las eventualidades . *********** equation (h) = promisesAreFulfilled(historyToSetFormula(h)) . > G F 'p < ('p,X G F 'p) < X G F 'p,F 'p (G F 'p < ('p,X G F 'p) < X G F 'p,F 'p) promisesAreFulfilled(historyToSetFormula(G F 'p < ('p,X G F 'p) < X G F que las premisas, en este caso p , se encuentra SetFormula y se obtiene una respuesta positiva. De esta forma sustituye por un nodo abierto. *********** equation eq (s:SetFormula,t:SetFormula) contain sInternal t:SetFormula = true . > ^ false,X G F 'p,X G F 'p,G F 'p,F 'p > 'p 40 (^ false U ^ p) F ^ 'q) < noH]D(noD) rewrites: 251 in 1628036047000ms cpu (4ms real) (0 rewrites/second) Durante la ejecución se detecta la existencia de se mostrarán los puntos . El nodo repetido es el de la fórmula eq S3[s:SetFormula < h2:History < s:SetFormula < h1:History]D(d) = (s:SetFormula < h2:History) < s:SetFormula < < G F 'p < (('p,X G F 'p) < X G F 'p,F 'p) < G F 'p < ('p,^ 'q,X G F 'p) < ('p,X G F 'p,F ^ 'q) < (X G F 'p,F 'p,F ^ 'q) < (G F 'p,F ^ ' q) para averiguar si se han cumplido las promisesAreFulfilled(historyToSetFormula(h)) . promisesAreFulfilled(historyToSetFormula(G F 'p < ('p,X G F 'p) < X G F , se encuentra n en el histórico De esta forma el bucle se sInternal t:SetFormula = true . ('p,^ false,X G F 'p,X G F 'p,G F 'p,F 'p) containsInternal 'p ---> true *********** equation eq true = ^ false . empty substitution true ---> ^ false 3.3. Comparación de resultados Para testear l as implementaciones expuestas en el apartado anterior testear el programa de forma más exhaustiva. Se han ejecutado 33 ejemplos (5). La herramienta TTM se rá nuestra referencia para comparar el coste temporal ya que se basa en el mismo algoritmo optimización que aquí no se optimización desactivada, de manera q i mportante es que la herramienta cosa que nuestro programa no hace, así que es de esperar que la herramienta TTM tarde más. A continuación se presenta n las dos versiones de la implementación en cuanto a lo hace en cuanto al tiempo resultados de la herramienta TTM, l la tercera los de la versión extendida de la misma Tabla 8: Comparación de la satisfacibilidad Test Satisfacible paqui1 Sí paqui2 Sí unsat1 No unsat2 No unsat3 No unsat4 No unsat5 No unsat6 No unsat7 No unsat8 No unsat9 No unsat10 No unsat11 No unsat12 No unsat13 No unsat14 No ('p,^ false,X G F 'p,X G F 'p,G F 'p,F 'p) containsInternal 'p *********** equation eq true = ^ false . empty substitution Comparación de resultados as implementaciones , primero se han utilizado las cinco pruebas globales expuestas en el apartado anterior . Al ver que éstas dan el resultado esperado testear el programa de forma más exhaustiva. ejemplos escogidos de las páginas de las herramientas T rá nuestra referencia para comparar el coste temporal ya que se mismo algoritmo utilizado para este proyecto. Sin embargo , se implementa, y por esta razón los ejemplos se ejecutarán optimización desactivada, de manera q ue la comparación tendrá más sentido mportante es que la herramienta , además de ejecutar el algoritmo, dibuja el árbol de salida, cosa que nuestro programa no hace, así que es de esperar que la herramienta TTM tarde más. n los resultados obtenidos en dos tablas: la primera tabla compara las dos versiones de la implementación en cuanto a la satisfacibilidad, mientras que la segunda tiempo de ejecución en segundos. La primera columna representa los resultados de la herramienta TTM, l a segunda los de la primera versión de la implementación y de la versión extendida de la misma . Comparación de la satisfacibilidad TlOrden TLOrdenExt Sí Sí Sí Sí No No No No ?? No ?? ?? No No No No No No No No No No No No No No No No No No No No 41 ('p,^ false,X G F 'p,X G F 'p,G F 'p,F 'p) containsInternal 'p utilizado las cinco pruebas globales esperado , se ha querido T RS tool (4) y TTM rá nuestra referencia para comparar el coste temporal ya que se , ésta utiliza una se ejecutarán con la ue la comparación tendrá más sentido . Otro detalle dibuja el árbol de salida, cosa que nuestro programa no hace, así que es de esperar que la herramienta TTM tarde más. dos tablas: la primera tabla compara satisfacibilidad, mientras que la segunda en segundos. La primera columna representa los de la primera versión de la implementación y desarrollado se usará la operación reutilizados. Tipos (Sorts) Lo primero que se necesita definir en un sistema son los tipos. cabo de la siguiente manera: sort sortId . Si se quiere definir varios tipos de golpe, sorts sortId1, sortId2, … , sortIdX . Nótese la importancia de que todas las instrucciones de un programa escrito en Maude acaben en un punto precedido por un espacio, Para establecer una jerarquía entre los tipos se definen los a no declarar ciclos en la jerarquía subsort sortId1 < sortId2 . subsort sortId2 < sortId3 . O bien: subsorts sortId1 < sortId2 < sortId3 . Operadores La sintaxis para declarar operadores es la siguiente: op opId : sortId1 sortId2 … sortIdX [operator attributes] . Si varios operadores comparten los mismos tipos, ops opId1 opId2: sortId1 sortId2 … sortOperator . Variables Se pueden declarar instancias de los tipos definidos para un sistema, para así poder d ecuaciones y reglas. Las variables se declaran de la siguiente forma: var N : tipoN . Si son varias variables del mismo tipo vars N M : tipoN . la operación protecting , ya que no se necesita modificar los módulos Lo primero que se necesita definir en un sistema son los tipos. La definición de tipos definir varios tipos de golpe, se puede utilizar la palabra sorts : sorts sortId1, sortId2, … , sortIdX . que todas las instrucciones de un programa escrito en Maude acaben en un punto precedido por un espacio, pues de lo contrario la compilación fallaría. Para establecer una jerarquía entre los tipos se definen los subtipos. Hay que prestar la jerarquía . subsort sortId1 < sortId2 . subsort sortId2 < sortId3 . subsorts sortId1 < sortId2 < sortId3 . La sintaxis para declarar operadores es la siguiente: op opId : sortId1 sortId2 … sortIdX -> [operator attributes] . Si varios operadores comparten los mismos tipos, se declaran de la siguiente forma: ops opId1 opId2: sortId1 sortId2 … sortIdX declarar instancias de los tipos definidos para un sistema, para así poder d Las variables se declaran de la siguiente forma: varias variables del mismo tipo : N M : tipoN . 48 necesita modificar los módulos La definición de tipos se lleva a que todas las instrucciones de un programa escrito en Maude acaben de lo contrario la compilación fallaría. Hay que prestar atención sortOperator de la siguiente forma: sortIdX -> declarar instancias de los tipos definidos para un sistema, para así poder d efinir sus Términos Un término es la aplicación de un operador a una variable o bien constante. Por ejemplo: opNameid1(N: tipoN) O bien _+_(N:Nat, M:Nat) Ecuaciones no condicionales Las ecuaciones se declaran mediante la palabra reservada eq termino1 = termino2 [atributos] T ambién existen las ecuaciones condicionales, pero no Atributos Los atributos pueden ser definidos para los operadores o las ecuaciones. Los atributos que serán utilizado s para la implementació assoc : Propiedad de asociatividad separar los términos que contengan el operador. Comm : Propiedad de conmutatividad, que significa que se puede intercambiar el orden de los operandos. (Id: término) : Define el elemento identidad del operador. Owise : El atributo de ecuación primera ecuación no cubre . Además permite imponer un orden para la ejecución de las ecuaciones de un mismo bloque Dominio de tipo (Kind) Es un concepto que no está definido por el propio usuario, a diferencia de los tipos. están agrupados implícitamente en componentes conexos. En algunos casos se puede cometer el error de que el resu ltado de una operación esté fuera del dominio de los tipos que lo definen. En este caso, una solución sería definir el tipo de éste resultado mediante su dominio, esto es, [tipoOperador]. Los dominios de ti define un término mediante éstos, es considerado un término de error. Reglas Las reglas son un instrumento para la reescrit siguiente: rl [etiqueta] : término1 => término2 [atributos] Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que si se encuentra una instancia de la parte izquierda en el estado actual, en el estado siguiente será reemplazado por la parte posibilidad de que la ejecución de varias reglas sea concurrente. es la aplicación de un operador a una variable o bien constante. Por ejemplo: opNameid1(N: tipoN) condicionales Las ecuaciones se declaran mediante la palabra reservada eq de la siguiente manera: termino1 = termino2 [atributos] ambién existen las ecuaciones condicionales, pero no se usarán en este programa. Los atributos pueden ser definidos para los operadores o las ecuaciones. Los atributos que s para la implementació n son los siguientes: asociatividad . Significa que no hace falta el uso de los paréntesis para separar los términos que contengan el operador. : Propiedad de conmutatividad, que significa que se puede intercambiar el orden de los : Define el elemento identidad del operador. : El atributo de ecuación otherwise permite expresar lo que pasa en los casos que . Además permite imponer un orden para la ejecución de las un mismo bloque owise . Es un concepto que no está definido por el propio usuario, a diferencia de los tipos. están agrupados implícitamente en componentes conexos. En algunos casos se puede cometer ltado de una operación esté fuera del dominio de los tipos que lo definen. En este caso, una solución sería definir el tipo de éste resultado mediante su dominio, Los dominios de ti po son supertipos de error, de e un término mediante éstos, es considerado un término de error. Las reglas son un instrumento para la reescrit ura en Maude. La sintaxis para é [etiqueta] : término1 => término2 [atributos] Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que si se encuentra una instancia de la parte izquierda en el estado actual, en el estado siguiente parte derecha de la regla. Lo más potente de e ste concepto es la posibilidad de que la ejecución de varias reglas sea concurrente. 49 es la aplicación de un operador a una variable o bien constante. Por ejemplo: de la siguiente manera: programa. Los atributos pueden ser definidos para los operadores o las ecuaciones. Los atributos que los paréntesis para : Propiedad de conmutatividad, que significa que se puede intercambiar el orden de los lo que pasa en los casos que la . Además permite imponer un orden para la ejecución de las Es un concepto que no está definido por el propio usuario, a diferencia de los tipos. Los tipos están agrupados implícitamente en componentes conexos. En algunos casos se puede cometer ltado de una operación esté fuera del dominio de los tipos que lo definen. En este caso, una solución sería definir el tipo de éste resultado mediante su dominio, po son supertipos de error, de e sta manera si se ura en Maude. La sintaxis para é stas es la Esto se utiliza para realizar una transición desde un estado a otro. Básicamente consiste en que si se encuentra una instancia de la parte izquierda en el estado actual, en el estado siguiente ste concepto es la Las reglas también pueden ser condicionales. Comandos de ejecución En esta sección se explicarán reduce [in module] term1 Reduce el término term1 , haciendo uso de los axiomas definidos sobre los tipos y las ecuaciones del módulo funcional. Puede reemplazarse por la palabra parte [in module] se tendrá en cuenta el módulo actual. Set trace on Este comando permitirá mostrar la traza completa de la ejecución de los comando Set trace off Esto hace lo contrario que el comando anterior. rewrite [n] [in module] term1 n : número máximo de paso s por aplicar. Reescribe el término term1 utilizando las ecuaciones, axiomas y reglas definidas en el módulo. Este comando hará tantas iteraciones como número de reglas aplicadas que se especifica por el usuario. Si no se especifica este número, se asu sustituirse por rew . Rewrite utiliza la estrategia de búsqueda el exterior (outermost). La estrategia en profundidad puede lleguen a ejecut arse, y puede que así la ejecución nunca termine. frewrite [n,m] [in module] term1 n : número máximo de reglas por aplicar. m : número máximo de reescrituras para un término. Este comando hace exactamente lo mismo que el explora las soluciones de izquierda a derecha, con el objetivo de que todas las reglas tengan la misma prioridad para decidir el curso de la ejecución. Esto podría resolver el inconveniente del comando termina. Sin embargo, el inconveniente es que puede que totalmente reducida. search [n, m] [in module] term1 tipoBusqueda term2 { Las reglas también pueden ser condicionales. los comandos de Maude que s erán de más utilidad. module] term1 , haciendo uso de los axiomas definidos sobre los tipos y las ecuaciones del módulo funcional. Puede reemplazarse por la palabra red . Si no se especifica la se tendrá en cuenta el módulo actual. Este comando permitirá mostrar la traza completa de la ejecución de los comando Esto hace lo contrario que el comando anterior. Se desactiva la visualización de la traza. [n] [in module] term1 s por aplicar. utilizando las ecuaciones, axiomas y reglas definidas en el módulo. Este comando hará tantas iteraciones como número de reglas aplicadas que se especifica por el usuario. Si no se especifica este número, se asu me que es infinito. El comando puede Rewrite utiliza la estrategia de búsqueda en profundidad (top down ) y ejecuta las reglas desde La estrategia en profundidad puede causar que haya reglas que arse, y puede que así la ejecución nunca termine. [n,m] [in module] term1 : número máximo de reglas por aplicar. : número máximo de reescrituras para un término. Este comando hace exactamente lo mismo que el rewrite , excepto que frewrite explora las soluciones de izquierda a derecha, con el objetivo de que todas las reglas tengan la misma prioridad para decidir el curso de la ejecución. resolver el inconveniente del comando rewrite , y asegurar que la ejecución el inconveniente es que puede que la solución obtenida no esté [n, m] [in module] term1 tipoBusqueda term2 { such that 50 erán de más utilidad. , haciendo uso de los axiomas definidos sobre los tipos y las . Si no se especifica la Este comando permitirá mostrar la traza completa de la ejecución de los comando s en Maude. desactiva la visualización de la traza. utilizando las ecuaciones, axiomas y reglas definidas en el módulo. Este comando hará tantas iteraciones como número de reglas aplicadas que se especifica por me que es infinito. El comando puede ) y ejecuta las reglas desde reglas que nunca frewrite no explora las soluciones de izquierda a derecha, con el objetivo de que todas las reglas tengan la asegurar que la ejecución la solución obtenida no esté condición} n : número máximo de soluciones existen sistemas en los que la ejecución no acab ejecución. m : La máxima profundidad de la búsqueda term1 : El término del que parte la búsqueda term2 : El término al que se quiere llegar. TipoBusqueda : La form a en que se efectuará la búsqueda del término de las que se dispone para el tipo de búsqueda son los siguientes: => 1 : El proceso de reescritura se realizará en un paso. => + : El proceso de reescritura se realizará en al menos un paso. => *: El proceso de reescritura se realizará en 0, 1, o muchos pasos. => !: El proceso de reescritura finalizará cuando se llegue a nodos finales. El comando search sigue la estrategia de búsqueda en anchura. Tiene la ventaja frente a los comandos rewrite y frewrite alcanzar el término deseado, lo cual garantiza el hecho de encontrar una solución si ésta existe. Continue number . El comando continue permite seguir con la ejecución viendo los siguientes profundidad, y se puede utilizar en el caso del definir nuevamente el número máximo de profundidad Código versión extendida A continuación se expone el código que resuelve los objetivos de este fmod TEMPLOGIC is protecting BOOL . protecting QID . *** TIPOS sorts Prop Literal Next LiNext Formula . sorts SetLiteral SetLiNext NESetFormula SetFormula . subsort Qid < Prop . subsort Bool < Prop . subsort Prop < Literal < LiNext < Formula . subsort Next < LiNext . subsort Literal < SetLiteral . subsort LiNext < SetLiNext . subsort Formula < NESetFormula < SetFormula . subsort SetLiteral < SetLiNext < NESetFormula . sort History . subsort SetFormula < History . número máximo de soluciones que se quiere encontrar. Este límite es importante porqu existen sistemas en los que la ejecución no acab aría, de esta forma se garantiza : La máxima profundidad de la búsqueda : El término del que parte la búsqueda . : El término al que se quiere llegar. a en que se efectuará la búsqueda del término term2 para el tipo de búsqueda son los siguientes: : El proceso de reescritura se realizará en un paso. : El proceso de reescritura se realizará en al menos un paso. El proceso de reescritura se realizará en 0, 1, o muchos pasos. El proceso de reescritura finalizará cuando se llegue a nodos finales. la estrategia de búsqueda en anchura. Tiene la ventaja frente a los frewrite de que realiza la búsqueda de diferentes formas para alcanzar el término deseado, lo cual garantiza el hecho de encontrar una solución si ésta permite seguir con la ejecución viendo los siguientes profundidad, y se puede utilizar en el caso del frewrite y rewrite también. número máximo de profundidad ( number) . versión extendida expone el código que resuelve los objetivos de este proyecto: Literal Next LiNext Formula . SetLiteral SetLiNext NESetFormula SetFormula . < Literal < LiNext < Formula . Literal < SetLiteral . LiNext < SetLiNext . Formula < NESetFormula < SetFormula . SetLiteral < SetLiNext < NESetFormula . SetFormula < History . 51 encontrar. Este límite es importante porqu e aría, de esta forma se garantiza el fin de la term2 . Las opciones la estrategia de búsqueda en anchura. Tiene la ventaja frente a los de que realiza la búsqueda de diferentes formas para alcanzar el término deseado, lo cual garantiza el hecho de encontrar una solución si ésta permite seguir con la ejecución viendo los siguientes niveles de también. Se puede proyecto: sorts Nodo SetNodos . subsort Nodo < SetNodos . sort Estado . ops S0 S1 S2 S3 S4 S5 SF : ops T0 T1 : *** VARIABLES vars h h1 h2 : History . vars s t : SetFormula . vars nes : NESetFormula . vars f g d : Formula . vars sl : SetLiteral . vars sln : SetLiNext . *** OPERADORES LOGICA TEMPORAL *** operadores de base op ^_ : Formula op ^_ : Next op ^_ : Prop op _/\ _ : Formula Formula op X_ : Formula op _U_ : Formula Formula *** operadores adicionales op _\ /_ : Formula Formula op _R_ : Formula Formula op G_ : Formula op F_ : Formula op _T_ : Formula Formula eq true = ^ false . eq f R g = ^ (^ f U ^ g) . eq f T g = ^ (f /\ ^ g) . *** NIVEL SETPROP op nil : op _,_ : SetFormula SetFormula op _,_ : SetFormula NESetFormula op _,_ : SetLiNext SetLiNext op _,_ : SetLiteral SetLiteral *** NIVEL NODO op _[_] D(_) : Estado History Formula op _;_ : SetNodos SetNodos op noD : -> Formula . *** HISTORY op noH : -> History . op _<_ : History History *** Estado 0 : contradicciones eq S0[(s, false ) < h] D(d) = SF[ eq S0[(s, f, ^ f) < h] D(d) = SF[ eq S0[h] D(d) = S1[h] D(d) [ *** Estado 0 : simplificacio eq S1[(^ false ) < h] D(d) eq S1[(nes, ^ false ) < h] D(d) = T1[nes < (nes, ^ eq S1[(nes, f, f) < h]D(d) eq S1[h] D(d) = S2[h] D(d) [ *** Estado 2 : literales eq S2[sl < h] D(d) = SF[^ eq S2[h] D(d) = S3[h] D(d) [ Nodo < SetNodos . S0 S1 S2 S3 S4 S5 SF : -> Estado . T0 T1 : -> Estado . h h1 h2 : History . s t : SetFormula . nes : NESetFormula . f g d : Formula . : SetLiteral . sln : SetLiNext . *** OPERADORES LOGICA TEMPORAL ^_ : Formula -> Formula . ^_ : Next -> LiNext . -> Literal . _ : Formula Formula -> Formula [comm assoc] . X_ : Formula -> Next . _U_ : Formula Formula -> Formula . *** operadores adicionales /_ : Formula Formula -> Formula [comm assoc] . _R_ : Formula Formula -> Formula . G_ : Formula -> Formula . F_ : Formula -> Formula . _T_ : Formula Formula -> Formula . f R g = ^ (^ f U ^ g) . ^ g) . nil : -> SetFormula . SetFormula -> SetFormula [comm assoc id: nil ] . _,_ : SetFormula NESetFormula -> NESetFormula [comm assoc id: nil ] . _,_ : SetLiNext SetLiNext -> SetLiNext [comm assoc id: nil ] . _,_ : SetLiteral SetLiteral -> SetLiteral [comm assoc id: nil ] . _[_] D(_) : Estado History Formula -> Nodo . _;_ : SetNodos SetNodos -> SetNodos [comm] . _<_ : History History -> History [assoc] . contradicciones ) < h] D(d) = SF[ false < (s, false ) < h] D(noD) . S0[(s, f, ^ f) < h] D(d) = SF[ false < (s, f, ^ f) < h] D(noD)[ S0[h] D(d) = S1[h] D(d) [ owise] . *** Estado 0 : simplificacio nes ) < h] D(d) = SF[(^ false) < h] D(noD) . ) < h] D(d) = T1[nes < (nes, ^ false ) < h] D(d) . S1[(nes, f, f) < h]D(d) = T1[(nes, f) < (nes, f, f)< h]D(d) [ S1[h] D(d) = S2[h] D(d) [ owise] . h] D(d) = SF[^ false < sl < h] D(d) . S2[h] D(d) = S3[h] D(d) [ owise] . 52 id: nil ] . id: nil ] . id: nil ] . id: nil ] . ) < h] D(noD) . < h] D(noD)[ owise] . ) < h] D(d) . = T1[(nes, f) < (nes, f, f)< h]D(d) [ owise] . *** Estado 3 : Histórico eq S3[s < h2 < s < h1] D(d) = SF[loopIsTrue(s < h2) < s < h2 < s < h eq S3[h] D(d) = S4[h] D(d) [ *** Estado 4 eq S4[sln < h]D(d) = T0[ next(sln) < sln < h] D(nextD(d)) . eq S4[h] D(d) = S5[h] D(d) [ *** Estado 5 *** ecuaciones tableaux eq S5[(s, (G f)) < h] D(d) = T0[(s, f, X(G f)) < (s, (G f)) < h] D(d) . eq S5[(s, ^(F f)) < h] D(d) = T0[(s, ^ f, ^ X(F f)) < (s, ^(F f)) < eq S5[(s, ^(f \ / g)) < h] D(d) = T0[(s, ^ f, ^ g) < (s, ^(f eq S5[(s, (f \ / g)) < h] D(d) = T0[(s, f) < (s, (f \ / g)) < h] D(d) ; T0[(s, g) < (s, (f \ / g)) < h] D(d) . eq S5[(s, (f U g)) < h] D(f U g) = T0[(s, g) < (s,(f U g)) < h] D(noD); T0[ (s, f, ^ g, X((^ toFormula(s) / < (s, (f U g)) < h ] D(X((^ toFormula(s) / eq S5[(s, d, (f U g)) < h] D(d) = T0[(s, d, g) < (s, d, (f U g)) < h] D(d); T0[(s, d, f, ^ g, X(f U g)) < (s, d, (f U g)) eq S5[(s,(f U g)) < h] D(d) = S5[(s, (f U g)) < h] D(f U g) [ eq S5[(s,(F f)) < h] D(F f) = T0[(s, f) < (s,(F f)) < h] D(noD) ; T0[(s, (^ f), X(^ toFormula(s) U f)) <(s, (F f)) < h] D(X(^ toFormula(s) U f)) . eq S5[(s, d , (F f)) < h] D(d) = T0[(s, d, f) < (s, d, (F f)) < h] D(d) ; T0[(s, d, (^ f), X(F f)) < (s, d, (F f)) < h] D(d) [ eq S5[(s, (F f)) < h] D(d) = S5[(s, (F f)) < h] D(F f) [ eq S5[(s, ^(G f)) < h] D(^(G f)) = T0[(s, ^ f) < (s,(G f)) < h] T0[(s, X((^ toFormula(s)) U (^ f))) < (s, (G f)) < h] D(X((^ toFormula(s)) U (^ f))) . eq S5[(s, d, ^(G f)) < h] D(d) = T0[(s, d, ^ f) < (s, d, (G f)) < h] D(d) ; T0[(s, d, ^ X(G f)) < (s, d, (G f)) < h] D(d) [ eq S5[(s, ^(G f)) < h] D (d) = S5[(s, ^(G f)) < h] D(^(G f)) [ *** FUNCIONES *** funciones para el Next op next_ : SetFormula - > SetFormula . eq next(s, X(f)) = next(s), f . S3[s < h2 < s < h1] D(d) = SF[loopIsTrue(s < h2) < s < h2 < s < h S3[h] D(d) = S4[h] D(d) [ owise] . next(sln) < sln < h] D(nextD(d)) . S4[h] D(d) = S5[h] D(d) [ owise] . S5[(s, (G f)) < h] D(d) = T0[(s, f, X(G f)) < (s, (G f)) < h] D(d) . S5[(s, ^(F f)) < h] D(d) = T0[(s, ^ f, ^ X(F f)) < (s, ^(F f)) < h] D(d) . / g)) < h] D(d) = T0[(s, ^ f, ^ g) < (s, ^(f \/ g)) < h] D(d) . / g)) < h] D(d) = / g)) < h] D(d) ; / g)) < h] D(d) . S5[(s, (f U g)) < h] D(f U g) = (s,(f U g)) < h] D(noD); T0[ (s, f, ^ g, X((^ toFormula(s) / \ f) U g)) ] D(X((^ toFormula(s) / \ f) U g)) . S5[(s, d, (f U g)) < h] D(d) = T0[(s, d, g) < (s, d, (f U g)) < h] D(d); T0[(s, d, f, ^ g, X(f U g)) < (s, d, (f U g)) < h] D(d) [owise ] . S5[(s,(f U g)) < h] D(d) = S5[(s, (f U g)) < h] D(f U g) [ owise] . S5[(s,(F f)) < h] D(F f) = T0[(s, f) < (s,(F f)) < h] D(noD) ; T0[(s, (^ f), X(^ toFormula(s) U f)) <(s, (F f)) < h] D(X(^ toFormula(s) U f)) . , (F f)) < h] D(d) = T0[(s, d, f) < (s, d, (F f)) < h] D(d) ; T0[(s, d, (^ f), X(F f)) < (s, d, (F f)) < h] D(d) [ owise] . S5[(s, (F f)) < h] D(d) = S5[(s, (F f)) < h] D(F f) [ owise] . S5[(s, ^(G f)) < h] D(^(G f)) = T0[(s, ^ f) < (s,(G f)) < h] D(noD) ; T0[(s, X((^ toFormula(s)) U (^ f))) < (s, (G f)) < h] D(X((^ toFormula(s)) U (^ f))) . S5[(s, d, ^(G f)) < h] D(d) = T0[(s, d, ^ f) < (s, d, (G f)) < h] D(d) ; T0[(s, d, ^ X(G f)) < (s, d, (G f)) < h] D(d) [ owise]. (d) = S5[(s, ^(G f)) < h] D(^(G f)) [ owise] . para el Next > SetFormula . next(s, X(f)) = next(s), f . 53 S3[s < h2 < s < h1] D(d) = SF[loopIsTrue(s < h2) < s < h2 < s < h 1]D(noD) . ] . eq next(s, ^ X(f)) = next(s), ^ f [ eq next(s, f) = next(s) [ eq next nil = nil . op nextD_ : Formula - > Formula . eq nextD(X(f)) = f . eq nextD(f) = noD [ owise *** funciones para la detección del bucle op loopIsTrue(_) : History eq loopIsTrue(h) = promisesAreFulfilled(historyToSetFormula(h)) . op historyToSetFormula(_) : History eq historyToSetFormula(s < h) = (s, historyToSetFormula(h)) . eq historyToSetFormula(s) = s . eq historyToSetFormula(noH) = nil . op promisesAreFulfilled(_) : SetFormula eq promisesAreFulfilled(s, eq promisesAreFulfilled(s) = (s contains promises(s)) [ op promises(_) : SetFormula eq promises(s, (f U g)) = (promises(s), g) . eq promises(s, (F g)) = (promises(s), g) [ eq promises(s, ^ (G g)) = (promises(s), ^ g) [ eq promises(s, f) = promises(s) [ eq promises(nil) = nil . op _contains_ : SetFormula SetForm eq s contains t = ((s, ^ op _containsInternal_ : SetFormula SetFormula eq (s, t) containsInternal t = eq s containsInternal t = op simplify(_) : SetFormula eq simplify(s, f, f) = simplify(s, f) . eq simplify(s) = s [ owise *** Convierte un SetFormula en su expr equivalente (, => / op toFormula_ : SetFormula eq toFormula(nil) = true eq toFormula(nes, f) = toFormula(nes) / eq toFormula(f) = f . *** SIMPLIFICACION *** *** limpieza historico eq SF[ false < s < h] D(d) = SF[ eq SF[(^ false ) < s < h] D(d) = SF[(^ *** reduccion arbol vars sn : SetNodos . eq SF[ false < h] D(d) ; sn = sn . eq SF[(^ false ) < h] D(d) ; sn = SF[(^ endfm mod TEMP-LOGIC-RULES is protecting TEMPLOGIC . vars h : History . vars d : Formula . rl [transition0] : T0[h] D(d) => S0[h] D(d) . rl [transition1] : T1[h] D(d) => S1[h] D(d) . next(s, ^ X(f)) = next(s), ^ f [ owise] . next(s, f) = next(s) [ owise] . next nil = nil . > Formula . owise ] . funciones para la detección del bucle loopIsTrue(_) : History -> Bool . loopIsTrue(h) = promisesAreFulfilled(historyToSetFormula(h)) . historyToSetFormula(_) : History -> SetFormula . historyToSetFormula(s < h) = (s, historyToSetFormula(h)) . historyToSetFormula(s) = s . historyToSetFormula(noH) = nil . promisesAreFulfilled(_) : SetFormula -> Bool . promisesAreFulfilled(s, false) = false . promisesAreFulfilled(s) = (s contains promises(s)) [ owise promises(_) : SetFormula -> SetFormula . promises(s, (f U g)) = (promises(s), g) . promises(s, (F g)) = (promises(s), g) [ owise] . promises(s, ^ (G g)) = (promises(s), ^ g) [ owise] . promises(s, f) = promises(s) [ owise] . promises(nil) = nil . _contains_ : SetFormula SetForm ula -> Bool . s contains t = ((s, ^ false) containsInternal simplify(t)) . _containsInternal_ : SetFormula SetFormula -> Bool . (s, t) containsInternal t = true . s containsInternal t = false [owise] . simplify(_) : SetFormula -> SetFormula . simplify(s, f, f) = simplify(s, f) . owise ] . *** Convierte un SetFormula en su expr equivalente (, => / \) toFormula_ : SetFormula -> Formula . true . toFormula(nes, f) = toFormula(nes) / \ f . toFormula(f) = f . < s < h] D(d) = SF[ false < noH] D(noD) . ) < s < h] D(d) = SF[(^ false) < noH] D(noD) . < h] D(d) ; sn = sn . ) < h] D(d) ; sn = SF[(^ false) < h] D(d) . [transition0] : T0[h] D(d) => S0[h] D(d) . [transition1] : T1[h] D(d) => S1[h] D(d) . 54 loopIsTrue(h) = promisesAreFulfilled(historyToSetFormula(h)) . owise ] . endm Pruebas unitarias En la sección siguiente se exponen las pruebas unitarias que se han realizado para comprobación del código. Para ello se han comentado las líneas que simplifican el historial, de forma proceso de reescritura, aunque en el caso de bifurcación de ramas solo se visualiza una rama, debido a la simplificación del árbol. En algunos casos la fórmula distinguida no es la esperada ya que la simplificación del historial es la que se ocupa de reemplazarla por rew toFormula(nil) . rew toFormula('p) . rew toFormula('p, 'q) . rew toFormula('p U 'q) . rew toFormula(nil, 'p) . rew S0[X(toFormula(('a U *** SF[^ false < ('b,'p,'q) < ('p,'q,('a U 'b)) *** < ('p /\ 'q /\ ('a U 'b)) < X ('p / rew simplify( 'p rew simplify( 'p, 'p rew simplify( 'p, 'q rew simplify( 'p, 'p, 'q rew simplify( 'p, 'p, 'q, 'q rew simplify(nil, 'p rew simplify(nil, 'p, 'p rew simplify(nil, 'p, 'q rew simplify(nil, 'p, 'p, 'q rew simplify(nil, 'p, 'p, 'q, 'q rew simplify(nil ) . rew ((nil ) contains (nil )) . rew (( 'p ) contains (nil )) . En la sección siguiente se exponen las pruebas unitarias que se han realizado para Para ello se han comentado las líneas que simplifican el historial, de forma que se pueda ver el proceso de reescritura, aunque en el caso de bifurcación de ramas solo se visualiza una rama, debido a la simplificación del árbol. En algunos casos la fórmula distinguida no es la esperada ya que la simplificación del historial que se ocupa de reemplazarla por noD en el caso del nodo final. rew toFormula(nil) . *** (^ false) . . *** ('p) . . *** ('p /\ 'q) . . *** ('p U 'q) . . *** ('p) . U 'b), 'p, 'q)) < noH] D(noD) . ('b,'p,'q) < ('p,'q,('a U 'b)) < ('p,'q /\ ('a U 'b)) ('a U 'b)) < X ('p / \ 'q /\ ('a U 'b)) < noH]D(noD) . ) . *** 'p . 'p, 'p ) . *** 'p . 'p, 'q ) . *** ('p, 'q) . 'p, 'p, 'q ) . *** ('p, 'q) . 'p, 'p, 'q, 'q ) . *** ('p, 'q) . ) . *** 'p . 'p, 'p ) . *** 'p . 'p, 'q ) . *** ('p, 'q) . 'p, 'p, 'q ) . *** ('p, 'q) . 'p, 'p, 'q, 'q ) . *** ('p, 'q) . rew simplify(nil ) . *** nil . ) contains (nil )) . *** ^ false . ) contains (nil )) . *** ^ false . 55 En la sección siguiente se exponen las pruebas unitarias que se han realizado para la que se pueda ver el proceso de reescritura, aunque en el caso de bifurcación de ramas solo se visualiza una rama, En algunos casos la fórmula distinguida no es la esperada ya que la simplificación del historial ('a U 'b)) ('a U 'b)) < noH]D(noD) . *** ^ false . *** ^ false . rew (( 'p, 'q) contains (nil )) . rew ((nil, 'p, 'q) contains (nil )) . rew ((nil ) contains ( rew (( 'p ) contains ( rew (( 'p, 'q) contains ( rew ((nil, 'p, 'q) contains ( rew ((nil ) contains (nil, rew (( 'p ) contains (nil, rew (( 'p, 'q) contains (nil, rew ((nil, 'p, 'q) contains (nil, rew ((nil ) contains (nil, rew (( 'p ) contains (nil, rew (( 'p, 'q) contains (nil, rew ((nil, 'p, 'q) contains (nil, rew ((nil ) contains ( rew (( 'p ) contains ( rew (( 'p, 'q) contains ( rew ((nil, 'p, 'q) contains ( rew ((nil ) contains (nil , rew (( 'p ) contains (nil , rew (( 'p, 'q) contains (nil , rew ((nil, 'p, 'q) contains (nil , rew ((nil ) contains ( rew (( 'p ) contains ( rew (( 'p, 'q) contains ( rew ((nil, 'p, 'q) contains ( rew ((nil ) contains (nil, rew (( 'p ) contains (nil, rew (( 'p, 'q) contains (nil, rew ((nil, 'p, 'q) contains (nil, rew ((nil ) contains (nil, rew (( 'p ) contains (nil, rew (( 'p, 'q) contains (nil, rew ((nil, 'p, 'q) contains (nil, rew ((nil ) contains ( contains (nil )) . *** ^ false . contains (nil )) . *** ^ false . rew ((nil ) contains ( 'p )) . *** false . ) contains ( 'p )) . *** ^ false . contains ( 'p )) . *** ^ false . contains ( 'p )) . ** * ^ false . rew ((nil ) contains (nil, 'p )) . *** false . ) contains (nil, 'p )) . *** ^ false . contains (nil, 'p )) . *** ^ false . contains (nil, 'p )) . *** ^ false . rew ((nil ) contains (nil, 'p, 'q )) . *** false . ) contains (nil, 'p, 'q )) . *** false . contains (nil, 'p, 'q )) . *** ^ false . contains (nil, 'p, 'q )) . *** ^ false . rew ((nil ) contains ( 'p, 'q )) . *** false . ) contains ( 'p, 'q )) . *** false . contains ( 'p, 'q )) . *** ^ false . contains ( 'p, 'q )) . *** ^ false . rew ((nil ) contains (nil , true)) . *** ^ false . ) contains (nil , true)) . *** ^ false . contains (nil , true)) . *** ^ false . contains (nil , true)) . *** ^ false . rew ((nil ) contains ( 'p , true)) . *** false . ) contains ( 'p , true)) . *** ^ false . contains ( 'p , true)) . *** ^ false . contains ( 'p , true)) . *** ^ false . rew ((nil ) contains (nil, 'p , true)) . *** false . ) contains (nil, 'p , true)) . *** ^ false . contains (nil, 'p , true)) . *** ^ false . contains (nil, 'p , true)) . *** ^ false . rew ((nil ) contains (nil, 'p, 'q, true)) . *** false . ) contains (nil, 'p, 'q, true)) . *** false . contains (nil, 'p, 'q, true)) . *** ^ false . contains (nil, 'p, 'q, true)) . *** ^ false . rew ((nil ) contains ( 'p, 'q, true)) . *** false . 56 *** ^ false . *** ^ false . *** false . *** ^ false . *** ^ false . * ^ false . *** false . *** ^ false . *** ^ false . *** ^ false . *** false . *** false . *** ^ false . *** ^ false . *** false . *** false . *** ^ false . *** ^ false . *** ^ false . *** ^ false . false . *** ^ false . *** false . *** ^ false . *** ^ false . *** ^ false . *** false . *** ^ false . *** ^ false . *** ^ false . *** false . *** false . *** ^ false . *** ^ false . *** false . rew (( 'p ) contains ( rew (( 'p, 'q) contains ( rew ((nil, 'p, 'q) contains ( rew ((nil ) contains ( rew (( 'p ) contains ( rew (( 'p, 'q) contains ( rew ((nil, 'p, 'q) contains ( rew promises(nil ) . rew promises(nil, 'p rew promises(nil, 'p, 'q rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises(nil, ('p U 'q rew promises(nil, ('p U true rew promises( 'p rew promises( 'p, 'q rew promises( ('p U 'q rew promises( ('p U true rew promises( ('p U 'q rew promises( ('p U true rew promises( ('p U 'q rew promises( ('p U true rew promises( ('p U 'q rew promises( ('p U true rew promises( ('p U 'q ) contains ( 'p, 'q, true)) . ** * false . contains ( 'p, 'q, true)) . *** ^ false . contains ( 'p, 'q, true)) . *** ^ false . rew ((nil ) contains ( true)) . *** ^ false . ) contains ( true)) . *** ^ false . contains ( true)) . *** ^ false . contains ( true)) . *** ^ false . rew promises(nil ) . *** (nil) . ) . *** (nil) . 'p, 'q ) . *** (nil) . 'q ), 'r ) . *** ('q) . true ), 'r ) . *** (^ false) . 'q ), 'r ) . *** ('q) . true ), 'r ) . *** (^ false) . 'q ), ('r U 's) ) . *** ('q, 's) . true ), ('r U 's) ) . *** (^ false, 's) . 'q ), ('r U 's) ) . *** ('q, 's) . true ), ('r U 's) ) . *** (^ false, 's) . 'q ), ('r U 's), 't) . *** ('q, 's) . true ), ('r U 's), 't) . *** (^ false, 's) . 'q ), ('r U 's), 't) . *** ('q, 's) . true ), ('r U 's), 't) . *** (^ false, 's) . ) . *** (nil) . 'p, 'q ) . *** (nil) . 'q ), 'r ) . *** ('q) . true ), 'r ) . *** (^ false) . 'q ), 'r ) . *** ('q) . true ), 'r ) . *** (^ false) . 'q ), ('r U 's) ) . *** ('q, 's) . true ), ('r U 's) ) . *** (^ false, 's) . 'q ), ('r U 's) ) . *** ('q, 's) . true ), ('r U 's) ) . *** (^ false, 's) . 'q ), ('r U 's), 't) . *** ('q, 's) . 57 * false . *** ^ false . *** ^ false . *** ^ false . *** ^ false . *** ^ false . *** ^ false . *** (^ false, 's) . *** (^ false, 's) . *** (^ false, 's) . *** (^ false, 's) . *** (^ false, 's) . *** (^ false, 's) .