Mostrando entradas con la etiqueta Verificación y validación de software. Mostrar todas las entradas
Mostrando entradas con la etiqueta Verificación y validación de software. Mostrar todas las entradas

domingo, 4 de noviembre de 2012

Lógica temporal lineal LTL

Sabemos que la máquina que provee los productos debe de ser recargada siempre que se termine el producto.

Esto puede formularse de la siguiente manera: la operación de recarga se produce un número infinito de veces. En un sistema con este tipo de limitaciones el sistema debe pasar por un estado que satisface alguna propiedad.
En el ejemplo de la maquina de productos, podemos tener este tipo de sistema por ejemplo decimos que los estudiantes compradores son infinitos.

El ejercicio que elegí es el siguiente:

EXERCISE 14.1 Formalize the following statements.


2. The beer storage becomes empty infinitely many times.

Entonces tenemos los siguientes conectivos y operadores temporales:

Imagen de http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14


Expresamos con "Y", "que la maquina se vacía , para decir que se vacía infinitamente usaremos los siguientes operadores temporales:

 Siempre

 Next

 Eventualmente

Expresamos con "Y", "que la maquina se vacía , para decir que se vacía infinitamente usaremos los siguientes operadores temporales:

Referencias

http://www.voronkov.com/lics_doc.cgi?what=chapter&n=14

lunes, 29 de octubre de 2012

Sistema de transiciones

Mi sistema es: Modelado de madera en un taller
Se compone de tres partes:

  • El material que se va a modelar: Es la pieza de madera que llega en bruto para poder ser procesada
  • La máquina que modela: Es la maquina que corta la madera
  • Un stock que guarda las piezas: Es en donde se almacenan los pedazos de madera cortados

Los componentes  a detalle los muestro a continuación:

La máquina se compone de :

  • Estados
    • Trabajando: Este estado se da cuando la máquina ya tiene el material y lo esta modelando.
    • Esperando: Se da cuando la máquina no tiene nada de material por modelar.
  • Transiciones
    • Se almacena: Cuando ya se termino de procesar la madera se almacena en el stock, de trabajando a esperando.
    • Empieza el tratamiento: Cuando apenas llega la madera, se empieza a tratar, de esperando a trabajando.



Material se compone de:
  • Estados
    • en bruto: se da cuando el material aun no se ha moldeado, asi como esta antes de procesarlo.
    • refinado: se da cuando el material ya fue procesado y esta listo para almacenarse
  • Transiciones
    • Se almacena: es cuando el material ya fue refinado esta listo para almacenarse
    • Va a tratamiento: Es la transición de en bruto a refinado.

Stock:
  • Estados
    • vacio: se da cuando le stock no tiene nunguna pieza almacenada
    • lleno: se da cuando ya no cabe otra pieza en el stock
  • Transiciones
    • se sacan las piezas: cambia el estado de lleno a vacio, quitando las piezas ya existentes para  poder meter más.
    • llega material: cambia el estado de vacio a lleno, cuando se estan guardando las piezas ya modeladas.



Diagrama de transiciones
Ahora juntamos todos los componentes en un grafo para poder ver el comportamiento del sistema en conjunto.
Material||Máquina||Stock

Estados:
1, 0 = Maquina (Trabajando, Esperando)
0, 1 = Material(En bruto, refinado)
0, 1 = Stock (vacío, lleno)

Transiciones:
1, 2, 3, 4, 5: llega el material, se almacena, va a tratamiento, empieza el tratamiento, se sacan las piezas.





martes, 23 de octubre de 2012

Red de petri

Las redes de Petri son una herramienta de modelado de sistemas secuenciales discretos y concurrentes. Usando las redes de Petri podemos visualizar el comportamiento dinámico de los sistemas. Y se forma por los siguientes elementos:
  • Lugares: Tienen acciones asociadas.
  • Transiciones: Evolucionan el sistema de un lugar a otro.
  • Arcos orientados: Unen lugares con transiciones o viceversa.
  • Marcas: Se ponen en los lugares y representan el estado del sistema en cada momento.
  • Lugar marcado: Un lugar que tiene por lo menos una marca.
  • Marcado de una red: El número de marcas y su situación en un instante determinado.
Una red de Petri es un grafo orientado con dos tipos de nodos: lugares(circunferencias) y transiciones(barras). Los arcos unen con una transición o viceversa. Un lugar puede tener un número positivo o nulo de marcas.

Se pueden asociar entradas y salidas a lugares y transiciones(p.e.: salida -> lugar marcado; entrada -> transición)

Una red de Petri es una tupla de 6 elementos (S, T, F, M0, W, K) Donde:

  • S son uno o más lugares.
  • T son las transiciones.
  • F son las flechas.

Ahora un ejemplo de un simple dibujo:





Tenemos:

  • Cuatro lugares, esto vienen siendo los círculos
  • Cuatro transiciones, vienen siendo las lineas negras
  • Nueve arcos, vienen siendo las flechas
  • 1 token (punto negro que se mueve)


Simulación con TAPAAL











El pasado fue un simple dibujo, ahora uno que tenga algún sentido:

Modelado de madera en un taller: un taller consiste en una máquina de corte y un stock. Cuando llega un pedido y la máquina de corte está disponible, el producto puede ser procesado (corte de operación). Una vez que el tratamiento se ha completado, el producto que ha sido procesado es almacenado. De otra manera, el producto debe esperar hasta que la máquina se libere antes de que pueda ser procesado.


Tenemos:

  • Cuatro lugares, esto vienen siendo los círculos
  • Tres transiciones, vienen siendo las lineas celestes.
  • Siete arcos, vienen siendo las flechas
  • 1 token, el producto a tratar.

Ahora a dibujarlo con Python:



Y así se ven las imágenes resultantes:



Referencias

Redes de Petri

sábado, 13 de octubre de 2012

Redes semánticas

Representación del conocimiento

[1]

Redes semánticas

Proporcionan ayuda gráfica para poder visualizar el conocimiento, así como algoritmos eficientes con los que se puede saber las propiedades de un objeto basándose en su pertenencia a una categoría.

En 1909 Charles Peirce propuso los grafos existenciales que es una notación gráfica de nodos y arcos. Existen variantes de Redes Semánticas pero todas pueden representar objetos, categorías de objetos y relaciones entre ellos. La notación común gráfica de las redes semánticas es ver los objetos o nombres de categorías en óvalos o cajas conectados con flechas etiquetados. Un ejemplo es:




En donde se puede ver que "Mary" es "MiembroDe" "PersonaFemenina", lo cual se formaliza con Mary ∈ PersonaFemenina.  De la misma manera tenemos la relación "Mary" "HermanoDe" "John" y se formaliza con HermanaDe(Mary, John).
En el dibujo también podemos ver que todas las "Personas" "tieneMadre" del sexo femenino, no es posible dibujar una relación desde "Personas" hasta "PersonasFemeninas" entonces se usa una notación especial como "- -" y se expresa:

∀x x∈Personas ⇒ [∀y TieneMadre(x,y)  ⇒ y ∈ PersonaFemenina]

Otra afirmación que podemos obtener es que las personas tienen dos piernas, por lo que:

∀x x∈Personas ⇒ Piernas(x, 2)

Hay que tener cuidado con no expresar que una categoría tiene piernas , la caja con linea simple se usa para expresar que los miembros pertenecientes a esa categoría tienen esa propiedad.

Este lenguaje se puede utilizar para el razonamiento de la herencia, por ejemplo "Mary" por el hecho de ser Persona sabemos que tiene dos piernas. Y para poder saber cuantas piernas tiene "Mary" en el grafo, se puede seguir el algoritmo de herencia que sigue el enlace "MiembroDe" desde "Mary" hasta la categoría a la cual pertenece, después continuar por el enlace "SubconjuntoDe" hasta que se encuentra la categoría en la que existe un enlace etiquetado con el recuadro Piernas, que sería Personas.
Es aquí donde se aplica la lógica predicativa ya que combinados la "lógica predicativa" con la red semántica se obtiene simplicidad y eficiencia para manejar el conocimiento de la información.

Gracias a la lógica predicativa es posible saber formalizar que si "Mary" es hermana de John entonces, entonces Jhon tiene una hermana que se llama "Mary". Así podemos obtener relaciones inversas "Tiene hermana" es lo inverso a "HermanaDe":

∀p, s TieneHermana(p, s) ⇔ HermanaDe(s, p)

Entonces ahora el chiste es pasar eso a la red semántica  para hacerlo hay que agregar una nueva relación entre John y Mary que sea un flecha que sale de John hacia Mary, y se llame TieneHermana.


Ahora teniendo la pregunta ¿Como se llama la hermana de John? podremos ir directamente a buscar en la relación "TieneHermana" desde John hasta Mary en vez de buscar en todas las personas de sexo femenino y buscar si esa persona tiene un enlace "HermanaDe" hacia "John".

Otra cosa que podemos agregar a la red son excepciones como por ejemplo John tiene una pierna, para esto primero formalizamos la expresión:


∀x, x∈Personas ^ x  ≠ John ⇒ Piernas(x,2)




Y así es como se sobrescribe la propiedad TienePiernas para John.

Este manera de manejar la información con red semántica, es realmente utilizada, actualmente existen Frameworks que partiendo de la lógica predicativa son capaces de crear un sistema de semántica para manejar el conocimiento, es ideal usarlo en sistemas como Bibliotecas o Sistemas internos para empresas que necesitan organizar la información de proyectos, empleados entre otras cosas.
Y son capaces de mostrarnos gráficos(grafos) de manera automática para representarnos la información.

[2]

Estos sistemas crean también las bases de datos con todo lo necesario para poder obtener las relaciones deseadas, la red semántica en la web es la Web Semántica que aunque son diferentes los conceptos parten de los mismos fundamentos, el lenguaje de Consulta RQL tiene una manera muy particular de mostrar las relaciones de Web Semántica con la lógica predicativa, por ejemplo el último ejemplo de John podríamos mostrarlo así, "Alguna persona masculina que tenga solo una pierna"

"Any N WHERE N name X, X MiembroDe Y, Y is PersonaMasculina, X tienePiernas 1"

El resultado de esta consulta seria el atributo Nombre de la Persona que solo tiene una pierna.


Fuentes

Russel, S., & Norving, P. (2004). Inteligencia artificial. (Pearson ed.). Madrid:

[1]  http://www.idatix.com/idatix-and-kmworld-unravel-the-mystery-of-knowledge-management/knowledge-management/

[2] http://www.cubicweb.org/blog/1238?__fromnavigation=1&__stop=19&__start=10&vid=primary

domingo, 16 de septiembre de 2012

Principios de demostraciones en validez


Para esta semana el ejercicio lo obtuve del pdf http://www.logicinaction.org/docs/ch4.pdf  y la manera de resolverlo también ya que venían ejemplos muy parecidos, es el siguiente:


Exercise 4.3 Translate the following sentences into predicate logical formulas:
(1) If John loves Mary, then Mary loves John too.
(2) John and Mary love each other.
(3) John and Mary don’t love each other.
(4) If John and Peter love Mary then neither Peter nor Mary loves John.


Ejercicio 4.3 Transforma las siguientes oraciones a formas lógicas predicativas:
(1) Si John ama a Mary, entonces Mary ama a John también.
(2) John y Mary sea aman uno al otro.
(3) John y Mary no se aman uno al otro.
(4) Si John y Peter aman a Mary entonces ni Peter ni Mary aman a John.


Podemos definir que X ama a Y con la siguiente y única expresión que necesitamos para transformar nuestros enunciados :
A(X, Y)


1. Si John ama a Mary, entonces Mary ama a John también. Entonces definimos con nuestra funcion A(X, Y) que recibe dos argumentos el primero la persona que hace la acción y el segundo quien la recibe. Al decir que John ama a Mary esto queda así: A(J, M) y como agregamos "entonces" osea una consecuencia de la primera agregamos el símbolo -> para ahora decir que Mary ama a John: A(M, J). Que queda como sigue:

A(J, M) ⇒ A(M, J)


2. John y Mary se aman uno al otro. En esta expresión a diferencia de la primera es que una cosa no es consecuencia de la otra lo que podemos agregar el conector lógico and para unir las nos funciones, una que exprese que John ama a Mary A(J, M)  y otra que Mary ama a John A(M, J).

A(J, M) ^ A(M, J)


3. John y Mary no se aman uno al otro. Es muy parecida a la anterior pero hay que negar las dos funciones, y las seguimos uniendo con un and.

¬(A(J, M) ^ A(M, J))


4. Si John y Peter aman a Mary entonces ni Peter ni Mary aman a John. Para expresar este enunciado en lógica predicativa tenemos que dividirlo en dos primero escribir que "John y Peter aman a Mary" con la expresión: A(J, M) ^ A(P, J) y después "ni Peter ni Mary aman a John" con la expresión:

¬A(P, J) ^ ¬A(M, J), y ahora si unirlas con el conector -> que expresa que Si John y Peter aman a Mary entonces ni Peter ni Mary aman a John:

(A(J, M) ^ A(P, M)) ⇒ (¬A(P, J) ^ ¬A(M, J))

sábado, 8 de septiembre de 2012

Lógica predicativa

El ejercicio de esta semana consite en encontrar la manera de expresar con lógica predicativa los siguientes enunciados tomados del libro "Lean Symbolic Logic", de Charles Dodgson, ejercicio 9 página 101:
 
 "John is in the house"
"Everybody in the house is ill."

"John esta en la casa"
"Todos en la casa están enfermos"

Aquí el Universo son las personas, decidí usar las siguientes expresiones(la x es una variable que le podremos dar valores con un cuantificador o con algúna persona en particular)

  • C(x) que significa que estan en Casa
  • E(x) significa que estan Enfermos

Ahora tenemos nuestra primera afirmación que dice "John esta en la casa" lo que podemos expresar así:

  • C(John)
    Que quiere decir Jhon esta en la casa
Y la siguiente afirmación es "Todos en la casa están enfermos", en donde podemos notar que tiene la palabra "Todos" lo cual expresamos con un cuantificador "" y lo formalizamos de la manera siguiente:

  • ∀x C(x)→E(x)
    Que expresa que Todas las personas que están en casa estan enfermas

Con estas dos expresiones podemos concluir por lógica que John esta enfermo, ya que Jhon esta en casa y todas las personas que estan en casa estan enfermas. Lo que expresamos así, primero sustitumos, luego sacamos nuestra conclusión:

Aquí estamos sustitituyendo la "x" por "Jhon",  x = Jhon,
C(John)→E(John)

  • ∴ E(John)

En solo expresiones la formalización de este argumento es la siguiente:

  • ∀x C(x)→E(x)
  • C(John)
  • ∴ E(John)




Referencias

Lógica de primer orden
Lógica predicativa de primer y segundo orden, Elisa Schaeffer

martes, 4 de septiembre de 2012

Diagrama binario de decisión

La tarea correspondiente a esta semana es la siguiente:
  • Inventen una expresión Booleana.
  • Usando por mínimo 3 variables y 4 conectivos básicos.
  • Construyan y dibujen su BDD.
  • Reduzcan el BDD resultante a un ROBDD.
  • Dibujen el ROBDD resultante.
La expresión booleana que yo inventé es:
ABCD + ¬A¬BCD + AB¬C¬D + AC¬B¬D

Como podemos apreciar cumple con los requisitos establecido, ya que tiene 4 variables y más de 6 conectivos básicos, en mi expresión "+" significa OR.

Primero cree una tabla de verdad:


Mi árbol binario queda de la siguiente manera, Líneas punteadas - - - quieren decir 0, y seguidas quieren decir 1:


El paso siguiente es hacer un BDD esto quiere decir Diagrama Binario de Decisión, en el que combinamos todos los subgrafos que sean iguales en uno solo y eliminar nodos cuyos hijos tengan la misma estructura, entonces queda de la siguiente manera, se reduce de 15 a 8 nodos:

Este fue el proceso que seguí, primero del nodo C derecho, abajo del B al lado derecho todos los números son ceros por eso se va esa C y redirecciono la línea de la B directo al 0, después el debajo de la B derecha, y C derecha tiene un nodo D izquierdo que también lo elimino ya que todo es 0 y se va a la cajita de 0. Lo mismo pasa con el nodo D que esta más a la izquierda todos sus números son 0 por eso lo elimino, enseguida se observa que debajo de las C que se encuentran debajo de la B izquierda hay dos D que tienen la misma combinación por lo que elimino una de las dos y redirecciono la línea al nodo correspondiente, después volvemos a tener dos nodos  con la misma combinación(0,1), entonces otra vez eliminamos uno de ellos y los juntamos en uno solo, para terminar solo dejamos una caja para 0 y otra para 1 y ahí juntamos todas las líneas. Esto se ve más claro en el gif siguiente:


Y ahora vemos el ROBDD(Reduce Ordered Binary Decision Diagram) para otros ordenes a ver que tanto se puede reducir, pero al parecer la forma más reducida de esta expresión fue la primera que obtuvimos ya que con varias combinaciones no logré bajarla de 8 nodos:

Orden C>D>A>B:
Orden C>D>B>A: 



Orden B>D>C>A:



Orden B>A>C>D:


Orden A>D>B>C:





Referencias:

Elisa Schaeffer
BDD


martes, 28 de agosto de 2012

Mapa de Karnaugh

Mapa de Karnaugh es un procedimiento directo para optimizar funciones booleanas con un máximo de 4 variables. Se pueden también hacer mapas con 5 o 6 variables pero estas son muy incómodas de usar.
El mapa es un diagrama que esta hecho con cuadros, cada cuadrado representa un mini-termino de la función.
Reconociendo diferentes patrones podemos derivar expresiones algebraicas alternativas para la misma función, de las cuales se puede seleccionar la más sencilla.
Las expresiones optimizadas que el mapa produce siempre se expresan en forma de suma de productos o producto de sumas.

Ahora si vamos a lo bueno, resolvamos algunos ejemplos que inventé con diferente número de variables:

Mapa de dos variables

F = ¬XY + ¬Y¬X + XY 

Lo primero que hay que hacer es construir la tabla de verdad:


Entonces hay que empezar a crear el Mapa-K, para esto creamos un 4 cuadros ya que teniendo dos variables son 4 las combinaciones posibles 2^2 = 4, los renglones representaran la X y las columnas la Y. De la siguiente manera:


Llenamos los cuadrantes de adentro con la respuesta correspondiente que obtuvimos en la tabla de verdad para la combinación indicada.


Tenemos que armar grupos de 1, solo podemos unir de manera vertical y horizontal, no en diagonal, y también nuestros grupos deben del tamaño correspondiente a una potencia de 2 (2, 4, 8, 16).
Entonces nos queda de la siguiente manera:


Lo siguiente es ahora si formar nuestra nueva expresión booleana:

Se hace así:

Tomamos la que esta encerrada en rojo, y queda solamente la X ya que la Y cambia de valores de 0 a 1, y como la X se mantiene constante solo tendremos X, pero como la X esta en 0 tenemos que ponerla negativa para que sea 1 entonces ya tenemos la ¬X.
Ahora de la que esta encerrada en azul vemos que la X cambia de valores entonces se queda la Y sola positiva.
La expresión final es: ¬X + Y
De tener al principio F = ¬XY + ¬Y¬X + XY ahora tenemos algo más pequeño F = ¬X + Y

Mapa de tres variables

Aquí tenemos que utilizar 3 variables por lo tanto este problema será un poquito más largo, he creado la siguiente función para mostrar el método:
F = ABC + A¬BC + AB¬C + ¬A¬B¬C + ¬A¬BC
Aquí esta la tabla de verdad:

a:
F = AB + CD



Ahora formamos el mapa-K, en este ejemplo de 3 variables tendremos 8 cuadrantes ya que hay 8 combinaciones posibles 2^3 = 8. La manera de distribuir las combinaciones es teniendo la A en los renglones y la B y C en las columnas, mostrando ahi todas las combinaciones posibles entre estas dos variables, el primer valor que aparece en el renglón como encabezado del mismo es el valor de la B, el segundo es el de la C.


A continuación empezamos a encerrar los grupos que más nos convengan, podemos ver que encerraremos en el primer renglón el grupo de unos, y en el segundo renglón tenemos un grupo de unos de 3 unos, lo que no es posible debido a que 3 no es potencia de dos por lo que tendremos que repetir algún termino que ya este en grupo lo cual es totalmente válido y nos quedara de la siguiente manera:


Entonces podemos ver del grupo rojo la expresión queda ¬A¬B (la C no debido a que cambia de 0 a 1), del grupo azul queda ¬BC (la A no porque cambia de 0 a 1) y del grupo azul vemos AB (la C no porque cambia). 
Y el resultado es de tener la expresión así: F = ABC + A¬BC + AB¬C + ¬A¬B¬C + ¬A¬BC
la hemos minimizado a: F = ¬A¬B + ¬BC + AB.


Mapa de cuatro variables

Ahora una función con 4 variables, usaremos esta expresión que se me ocurrió para mostrar el ejemplo:
F = ABCD + ¬ABCD + A¬BCD + AB¬CD + ABC¬D + ¬A¬BCD + AB¬C¬D

Tabla de verdad:


Lo que sigue es formar el mapa de 4x4 osea 16 cuadrantes que se forman de las combinaciones 2^4 = 16, ahora los renglones los forman A y B con todas sus combinaciones posibles, y las columnas C y D también con todas las combinaciones:


Ahora formamos los grupos de unos, recordemos que tienen que ser potencias de 2, nos quedó bastante cómodo el ejemplo, en la siguiente imagen les muestro como es que podemos resolver nuestro mapa:

Podemos empezar a formar la expresión simplificada tomando el circulo que queramos, yo elegí el rojo, entonces nos queda AB (C y D no porque cambian de valores) y del circulo azul nos queda CD (A y B no porque cambian de valores).
Nuestra expresión paso de ser así:
F = ABCD + ¬ABCD + A¬BCD + AB¬CD + ABC¬D + ¬A¬BCD + AB¬C¬D
a:
F = AB + CD

Y finalmente les muestro como es que compruebo las expresiones, no crean que lo hago manualmente, uso un programita muy sencillo de python, y es así como me puedo dar cuenta que lo optimicé correctamente.


La ejecución:




Referencias

domingo, 26 de agosto de 2012

Aplicación de la lógica proposicional

Lógica proposicional

Es una parte de la lógica que se encarga de estudiar la formación de proposiciones complejas partiendo de proposiciones simples.
Es un sistema formal en donde los elementos más simples representan proposiciones, y los conectivos representan operaciones entre las proposiciones, y asi se forman proposiciones de mayor complejidad.

La tarea asignada para esta semana es la siguiente:
"Investiguen aplicaciones de la lógica proposicional y documenten uno en su tercera tarea."

Yo elegí documentar la aplicación de la lógica proposicional en el diseño de los circuitos digitales.

[1]



Puertas lógicas

Podemos pensar en un circuito digital como una caja negra, en donde podemos crear relaciones entre las entradas y la salida.

La operación del circuito la podemos especificar al construir una tabla de entradas y salidas, en donde mostremos todos los posibles valores de entrada y de salida.

Para describir como operan los circuitos digitales es necesario introducir nociones matemáticas que especifica la operación de cada puerta y que es usado para diseñar y analizar circuitos.

Para representar una oración de lógica proposicional como circuito digital usamos las compuertas lógicas.
Las puertas lógicas son circuitos electrónicos que toman una o más señales de entrada para producir una señal de salida. Las señales eléctricas como voltaje o corriente existen en los sistemas digitales. Los circuitos que usan los voltajes tienen dos rangos separados de voltajes que representan valores binarios igual a 1 lógico o 0 lógico.
Como podemos ver que es posible representar estos valores con una tabla de verdad, es correcto decir entonces que los circuitos digitales los podemos representar con lógica proposicional.


[2]

Las compuertas lógicas aceptan señales entre 0 y 1 osea dentro del rango permitido y responden a los terminales de salida con señales binarias también. Las regiones entre 0 y 1 o 1 y 0 se llaman regiones de transito y este cambio se le llama transición.

Los simbolos usados para representar los tipos de compuertas los muestro a continuación:


[3]


Las puertas son circuitos electrónicos que producen como salida 0 o 1 de acuerdo a la tabla de verdad y los valores de entrada.

[4]

Actualmente TODOS los circuitos lógicos utilizados en los diseños electrónicos se pueden construir a partir de componentes electrónicos encapsulados en un chip, muchas veces se agrupan las compuertas en  uno solo, aunque posiblemente aun podamos encontrar solo la función lógica que necesitamos en un chip. Los elementos básicos de los circuitos digitales son las compuertas lógicas.

Les dejo un ejemplo de un circuito digital que inventé F = (¬X^Y) | (X^Z) utiliza compuertas lógicas, realizado con el Software Qucs:



Tabla de entrada/salida:




Refrencias

[1], [4] Puertas Lógicas
[2] AND, OR, NOT
[3] Símbolos puertas lógicas
Lógica proposicional, Elisa Schaeffer