diff --git a/Ejercicios Spin/Ej4.pml b/Ejercicios Spin/Ej4.pml new file mode 100644 index 0000000..a6e06b5 --- /dev/null +++ b/Ejercicios Spin/Ej4.pml @@ -0,0 +1,37 @@ +/* Ejercicio 4*/ + +byte button=0; + +/*estado 0 es luz off y estado 1 es luz on*/ +byte state; + +active proctype light(){ + state=0; + do + :: (state==0) -> atomic{ + if + :: (button) -> state=1; printf("enciende"); button=0; + fi + } + :: (state==1) -> atomic{ + if + :: (button) -> state=0; printf("apaga"); button=0; + fi + } + od +} + +active proctype entorno(){ + do + ::true -> button=1 + ::true -> skip + od; +} + +ltl spec1{ + []( ((state==0)&&button) -> <> (state==1)) +} + +ltl spec2{ + []( ((state==1)&&button) -> <> (state==0)) +} \ No newline at end of file diff --git a/Ejercicios Spin/Ej5.pml b/Ejercicios Spin/Ej5.pml new file mode 100644 index 0000000..b189e39 --- /dev/null +++ b/Ejercicios Spin/Ej5.pml @@ -0,0 +1,52 @@ +/* Ejercicio 5*/ + +byte timer=0; +byte button=0; +byte presencia=0; + +/*estado 0 es luz off y estado 1 es luz on*/ +byte state; + +active proctype light(){ + state=0; + do + :: (state==0) -> atomic{ + if + :: button -> state=1; printf("enciende"); button=0; + :: presencia -> state=1; printf("enciende"); presencia=0; + fi + } + :: (state==1) -> atomic{ + if + :: button&&!timer -> state=0; printf("apaga"); button=0; + :: timer&&!button -> state=0; printf("apaga"); timer=0; + :: timer&&button -> state=0; printf("apaga"); button=0; timer=0; + fi + } + od +} + +active proctype entorno(){ + do + ::true -> button=1 + ::true -> presencia=1 + ::true -> timer=1; + ::true -> skip + od +} + +ltl spec1{ + []( presencia -> <>(state==1)) +} + +ltl spec2{ + []( (state==1&&button) -> <>(state==0)) +} + +ltl spec3{ + []( (state==1&&timer) -> <>(state==0)) +} + +ltl spec4{ + []( ((state==0)&&button) -> <>(state==1)) +} diff --git a/Ejercicios Spin/Ej6_A.pml b/Ejercicios Spin/Ej6_A.pml new file mode 100644 index 0000000..0ed7abd --- /dev/null +++ b/Ejercicios Spin/Ej6_A.pml @@ -0,0 +1,72 @@ +/* Ejercicio 6*/ + +byte timer=0; +byte button=0; +byte presencia=0; +byte alarma_EN=0; + +/*estado 0 es luz off, estado 1 es luz on y estado 2 es alarma on*/ +byte state; + +active proctype light(){ + state=0; + do + :: (state==0) -> atomic{ + if + :: button -> state=1; printf("enciende"); button=0; + :: presencia&&(!alarma_EN) -> state=1; printf("enciende"); presencia=0; + :: presencia&&alarma_EN -> state=2; printf("enciende"); printf("alarma"); presencia=0; + fi + } + :: (state==1) -> atomic{ + if + :: button&&!timer -> state=0; printf("apaga"); button=0; + :: timer&&!button -> state=0; printf("apaga"); timer=0; + :: timer&&button -> state=0; printf("apaga"); button=0; timer=0; + :: (presencia&&alarma_EN&&!button&&!timer) -> state=2; printf("enciende"); printf("alarma"); presencia=0; + :: (presencia&&!alarma_EN&&!button&&!timer) -> state=1; printf("enciende"); presencia=0; + fi + } + :: (state==2) -> atomic{ + if + :: !alarma_EN -> state=0; printf("fin alarma"); + fi + } + + od +} + +active proctype entorno(){ + do + ::true -> timer=1; + ::true -> button=1 + ::true -> presencia=1 + ::true -> alarma_EN=1 + ::true -> alarma_EN=0 + ::true -> skip + od +} + +ltl spec1{ + []( ((state==1)&&(button)) -> <>(state==0)) +} + +ltl spec2{ + []( (state==1&&button) -> <>(state==0)) +} + +ltl spec3{ + []( (state==1&&timer) -> <>(state==0)) +} + +ltl spec4{ + []( ((state==1)&&(presencia&&alarma_EN&&!button&&!timer))) -> <>(state==2)) +} + +ltl spec5{ + []( ((state==1)&&(presencia&&!alarma_EN&&!button&&!timer)) -> <>(state==1)) +} + +ltl spec6{ + []( ((state==2)&&!alarma_EN) -> <>(state==0)) +} \ No newline at end of file diff --git a/Ejercicios Spin/Ej6_B.pml b/Ejercicios Spin/Ej6_B.pml new file mode 100644 index 0000000..b1ae0e1 --- /dev/null +++ b/Ejercicios Spin/Ej6_B.pml @@ -0,0 +1,62 @@ +/* Ejercicio 6*/ + +byte timer=0; +byte button=0; +byte presencia=0; +byte alarma_EN=0; + +/*estado 0 es luz off, estado 1 es luz on y estado 2 es luz on y alarma on*/ +byte state; + +active proctype light(){ + state=0; + do + :: (state==0) -> atomic{ + if + :: button -> state=1; printf("enciende"); button=0; + :: presencia&&(!alarma_EN) -> state=1; printf("enciende"); presencia=0; + :: presencia&&alarma_EN -> state=2; printf("enciende"); printf("alarma"); presencia=0; + fi + } + :: (state==1) -> atomic{ + if + :: (button||timer) && (!presencia) -> state=0; printf("apaga"); button=0; + :: (presencia&&alarma_EN) -> state=2; printf("enciende"); printf("alarma"); presencia=0; + :: (presencia&&(!alarma_EN)) -> state=1; printf("enciende"); presencia=0; + fi + } + :: (state==2) -> atomic{ + if + :: !alarma_EN -> state=0; printf("fin alarma"); + fi + } + + od +} + +active proctype entorno(){ + do + ::true -> timer=1; + ::true -> button=1 + ::true -> presencia=1 + ::true -> alarma_EN=1 + ::true -> alarma_EN=0 + ::true -> skip + od +} + +ltl spec1{ + []( ((state==1)&&(button||timer)&&(!presencia)) -> <>(state==0)) +} + +ltl spec2{ + []( ((state==1)&&(presencia&&alarma_EN))) -> <>(state==2)) +} + +/*ltl spec3{ + []( ((state==1)&&(presencia&&(!alarma_EN))) -> <>(state==1)) +}*/ + +ltl spec4{ + []( ((state==2)&&(!alarma_EN)) -> <>(state==0)) +} \ No newline at end of file diff --git a/Ejercicios Spin/Ej7.pml b/Ejercicios Spin/Ej7.pml new file mode 100644 index 0000000..6aeb586 --- /dev/null +++ b/Ejercicios Spin/Ej7.pml @@ -0,0 +1,102 @@ +/* Ejercicio 7*/ + +byte timer=0; +byte button=0; +byte presencia=0; +byte alarma_EN=0; + +int code_1=0; +int code_2=0; +int code_3=0; + +int pass_1=5; +int pass_2=3; +int pass_3=8; + +int count=0; + +/*estado 0 es luz off, estado 1 es luz on, estado 2 es alarma on y estado 3 es introduccion de codigo*/ +byte state; + +active proctype light(){ + state=0; + do + :: (state==0) -> atomic{ + if + :: button -> state=1; printf("enciende"); button=0; + :: presencia&&(!alarma_EN) -> state=1; printf("enciende"); presencia=0; + :: presencia&&alarma_EN -> state=2; printf("enciende"); printf("alarma"); presencia=0; count=0; code_1=0; code_2=0; code_3=0; + fi + } + :: (state==1) -> atomic{ + if + :: button&&!timer -> state=0; printf("apaga"); button=0; + :: timer&&!button -> state=0; printf("apaga"); timer=0; + :: timer&&button -> state=0; printf("apaga"); button=0; timer=0; + :: (presencia&&alarma_EN&&!button&&!timer) -> state=2; printf("enciende"); printf("alarma"); presencia=0; count=0; code_1=0; code_2=0; code_3=0; + :: (presencia&&!alarma_EN&&!button&&!timer) -> state=1; printf("enciende"); presencia=0; + fi + } + :: (state==2) -> atomic{ + if + :: !alarma_EN -> state=0; printf("fin alarma"); + :: button&&count==0 -> state=3; printf("introducir digito 1"); code_1++; + :: button&&count==1 -> state=3; printf("introducir digito 2"); code_2++; + :: button&&count==2 -> state=3; printf("introducir digito 3"); code_3++; + fi + } + :: (state==3) -> atomic{ + if + :: button&&count==0 -> state=3; printf("pulsado"); button=0; code_1++; + :: button&&count==1 -> state=3; printf("pulsado"); button=0; code_2++; + :: button&&count==2 -> state=3; printf("pulsado"); button=0; code_3++; + :: timer&&count<3 -> state=2; printf("digito introducido"); count++; + :: timer&&count>=3&&code_1==pass_1&&code_2==pass_2&&code_3==pass_3 -> state=0; printf("fin alarma"); count=0; code_1=0; code_2=0; code_3=0; + :: timer&&count>=3&&(code_1!=pass_1||code_2!=pass_2||code_3!=pass_3) -> state=2; printf("codigo incorrecto"); count=0; code_1=0; code_2=0; code_3=0; + fi + } + od +} + +active proctype entorno(){ + do + ::true -> timer=1 + ::true -> button=1 + ::true -> presencia=1 + ::true -> alarma_EN=1 + ::true -> alarma_EN=0 + ::true -> skip + od +} + +ltl spec1{ + []( ((state==1)&&(button)) -> <>(state==0)) +} + +ltl spec2{ + []( (state==1&&button) -> <>(state==0)) +} + +ltl spec3{ + []( (state==1&&timer) -> <>(state==0)) +} + +ltl spec4{ + []( ((state==1)&&(presencia&&alarma_EN&&!button&&!timer)) -> <>(state==2)) +} + +ltl spec5{ + []( ((state==1)&&(presencia&&!alarma_EN&&!button&&!timer)) -> <>(state==1)) +} + +ltl spec6{ + []( ((state==2)&&!alarma_EN) -> <>(state==0)) +} + +ltl spec7{ + []( ((state==3)&&count>=3&&code_1==pass_1&&code_2==pass_2&&code_3==pass_3) -> <>(state==2)) +} + +ltl spec8{ + []( ((state==3)&&count>=3&&(code_1!=pass_1||code_2!=pass_2||code_3!=pass_3)) -> <>(state==3)) +} \ No newline at end of file diff --git a/fsm/Makefile b/fsm/Makefile index 552fa12..946b59f 100644 --- a/fsm/Makefile +++ b/fsm/Makefile @@ -1,16 +1,10 @@ CC=gcc -CFLAGS=-g -Wall -ansi -O -I. -DNDEBUG -LDFLAGS=-L. -LDLIBS=-lwiringPi +CFLAGS=-g -Wall -O -I. -DNDEBUG -all: libwiringPi.a main interruptor +all: main -main: main.o fsm.o -interruptor: interruptor.o fsm.o +main: main.o reactor.o codigo_alarma.o principal.o timeval_helper.o fsm.o clean: - $(RM) *.o *~ main interruptor libwiringPi.a - -libwiringPi.a: wiringPi.o - ar rcs $@ $^ + $(RM) *.o *~ main diff --git a/fsm/codigo_alarma.c b/fsm/codigo_alarma.c new file mode 100644 index 0000000..43d7139 --- /dev/null +++ b/fsm/codigo_alarma.c @@ -0,0 +1,78 @@ +#include "timeval_helper.h" +#include +#include +#include +#include +#include +#include "codigo_alarma.h" + +extern int boton_alarma; // variable compartida +extern int alarma_EN; +char clave[3] = {2,1,1}; //la clave que debe ser introducida correctamente +char codigo[3]; +char indice = 0; +int count = 0; +struct timeval referencia; + +static int transicion_01 (fsm_t* this) { + return boton_alarma; +} + +static void salida_01 (fsm_t* this) { + gettimeofday (&referencia, NULL); + static struct timeval t_espera = { 3, 0 }; + timeval_add (&referencia, &referencia, &t_espera); + count++; +} + +static int transicion_22a (fsm_t* this) { + gettimeofday(&now, NULL); + check = timeval_less(&referencia, &now); + return boton_alarma&&(!check); +} + +static void salida_22a (fsm_t* this) { + count++; + //delay(200)//???? como se hace aqui? para filtrar rebotes +} + +static int transicion_22b (fsm_t* this) { + gettimeofday(&now, NULL); + check = timeval_less(&referencia, &now); + return boton_alarma&✓ +} + +static void salida_22b (fsm_t* this) { + if (count>=10){codigo[indice]=0;} + else{ codigo[indice]=count;} + indice++; + count=0; +} + +static int transicion_23 (fsm_t* this) { + if (indice >= 3) {return 1;} + else{ return 0;} +} + +static void salida_23 (fsm_t* this) { + //no hago nada +} + +static int transicion_30 (fsm_t* this) { + if ((codigo[0]==clave[0])&&(codigo[1]==clave[1])&&(codigo[2]==clave[2])){ + alarma_EN = !alarma_EN; + } + return true; +} + +fsm_t* fsm_new_alarma () +{ + static fsm_trans_t tt[] = { + { 0, transicion_01, 1, salida_01 }, + { 2, transicion_22a, 2, salida_22a}, + { 2, transicion_22b, 2, salida_22b}, + { 2, transicion_23, 3, salida_23}, + { -1, NULL, -1, NULL } + }; + return fsm_new (tt); +} \ No newline at end of file diff --git a/fsm/codigo_alarma.h b/fsm/codigo_alarma.h new file mode 100644 index 0000000..3516710 --- /dev/null +++ b/fsm/codigo_alarma.h @@ -0,0 +1,9 @@ +#ifndef CODIGO_ALARMA_H +#define CODIGO_ALARMA_H + +#include +#include "fsm.h" + +fsm_t* fsm_new_codigo_alarma(void); + +#endif \ No newline at end of file diff --git a/fsm/fsm.c b/fsm/fsm.c index a6ad630..356ee22 100644 --- a/fsm/fsm.c +++ b/fsm/fsm.c @@ -1,19 +1,14 @@ /* Mealy FSM implementation - Copyright (C) 2017 by Jose M. Moya - This file is part of GreenLSI Unlessons. - This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. - This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. - You should have received a copy of the GNU General Public License along with this program. If not, see . */ @@ -47,5 +42,4 @@ fsm_fire (fsm_t* this) break; } } -} - +} \ No newline at end of file diff --git a/fsm/fsm.h b/fsm/fsm.h index ab81e02..cf5c00a 100644 --- a/fsm/fsm.h +++ b/fsm/fsm.h @@ -1,19 +1,14 @@ /* Mealy FSM public interface - Copyright (C) 2017 by Jose M. Moya - This file is part of GreenLSI Unlessons. - This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. - This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. - You should have received a copy of the GNU General Public License along with this program. If not, see . */ @@ -41,4 +36,4 @@ fsm_t* fsm_new (fsm_trans_t* tt); void fsm_init (fsm_t* this, fsm_trans_t* tt); void fsm_fire (fsm_t* this); -#endif +#endif \ No newline at end of file diff --git a/fsm/principal.c b/fsm/principal.c new file mode 100644 index 0000000..0655026 --- /dev/null +++ b/fsm/principal.c @@ -0,0 +1,91 @@ +#include "principal.h" +#include "timeval_helper.h" +#include +#include +#include +#include +#include +#include "codigo_alarma.h" + +extern int boton_alarma; // boton codigo alarma +extern int boton; // encender y apagar luz +extern int presencia; // encender luz y alarma +extern int alarma_EN; +static struct timeval t_ref; + +static int transicion_01 (fsm_t* this) { + if (boton || (presencia&&(!alarma_EN))){ + return 1; + else{ + return 0; + } +} + +static void enciende_luz (fsm_t* this) { + static struct timeval t_espera = { 60, 0 }; + gettimeofday (&t_ref, NULL); + timeval_add (&t_ref, &t_ref, &t_espera); + printf ("******* Luz ON *******\n"); + boton = 0; + presencia=0; +} + +static int transicion_10 (fsm_t* this) { + struct timeval now; + gettimeofday (&now, NULL); + timeout = timeval_less (&t_ref, &now); + if ( (boton&&(!presencia)) || timeout) { + return 1; + } + else{ + return 0; + } +} + +static void apaga (fsm_t* this) { + printf ("******* Luz OFF *******\n"); + printf("******* Sonido OFF *******\n"); + //Independientemente de que el sonido ya estuviese apagado + boton = 0; + presencia = 0; +} + +static int transicion_11 (fsm_t* this) { + return presencia&&!alarma_EN; +} + +static int transicion_12 (fsm_t* this) { + return presencia&&alarma_EN; +} + +static void enciende_sonido(fsm_t* this) { + printf("******* Sonido ON *******\n"); + presencia=0; + boton=0; +} + +static int transicion_20 (fsm_t* this) { + return !alarma_EN; +} + +static void enciende_todo(fsm_t* this) { + printf("******* Sonido ON *******\n"); + printf ("******* Luz ON *******\n"); + presencia=0; + boton=0; +} + +fsm_t* fsm_new_luz () +{ + static fsm_trans_t tt[] = { + { 0, transicion_01, 1, enciende_luz }, + { 0, transicion_02, 2, enciende_todo}, + { 1, transicion_10, 0, apaga}, + { 1, transicion_11, 1, enciende_luz}, + { 1, transicion_12, 2, enciende_sonido}, + { 2, transicion_20, 0, apaga}, + { -1, NULL, -1, NULL } + }; + return fsm_new(tt); +} + diff --git a/fsm/principal.h b/fsm/principal.h new file mode 100644 index 0000000..371591e --- /dev/null +++ b/fsm/principal.h @@ -0,0 +1,9 @@ +#ifndef PRINCIPAL_H +#define PRINCIPAL_H + +#include +#include "fsm.h" + +fsm_t* fsm_new_principal(void); + +#endif \ No newline at end of file diff --git a/fsm/timeval_helper.c b/fsm/timeval_helper.c new file mode 100644 index 0000000..9898324 --- /dev/null +++ b/fsm/timeval_helper.c @@ -0,0 +1,33 @@ +#include + +int +timeval_less (const struct timeval* a, const struct timeval* b) +{ + return (a->tv_sec == b->tv_sec)? (a->tv_usec < b->tv_usec) : + (a->tv_sec < b->tv_sec); +} +// timeval add hace a+b +void +timeval_add (struct timeval* res, + const struct timeval* a, const struct timeval* b) +{ + res->tv_sec = a->tv_sec + b->tv_sec; + res->tv_usec = a->tv_usec + b->tv_usec; + if (res->tv_usec >= 1000000) { + res->tv_sec += res->tv_usec / 1000000; + res->tv_usec = res->tv_usec % 1000000; + } +} + +void +timeval_sub (struct timeval* res, + const struct timeval* a, const struct timeval* b) +{ + res->tv_sec = a->tv_sec - b->tv_sec; + res->tv_usec = a->tv_usec - b->tv_usec; + if (res->tv_usec < 0) { + res->tv_sec --; + res->tv_usec += 1000000; + } +} + diff --git a/fsm/timeval_helper.h b/fsm/timeval_helper.h new file mode 100644 index 0000000..502f4e1 --- /dev/null +++ b/fsm/timeval_helper.h @@ -0,0 +1,13 @@ +#ifndef TIMEVAL_HELPER_H +#define TIMEVAL_HELPER_H + +#include + +int timeval_less (const struct timeval* a, const struct timeval* b); +void timeval_add (struct timeval* res, + const struct timeval* a, const struct timeval* b); +void +timeval_sub (struct timeval* res, + const struct timeval* a, const struct timeval* b); + +#endif diff --git a/reactor/main.c b/reactor/main.c index 7a2bf4e..2dfef63 100644 --- a/reactor/main.c +++ b/reactor/main.c @@ -1,29 +1,85 @@ #include #include "reactor.h" +#include "principal.h" +#include "codigo_alarma.h" +#include "timeval_helper.h" -static -void -task1_func (struct event_handler_t* this) +fsm_t* principal; +fsm_t* codigo_alarma; + +int boton_alarma; +int boton; +int presencia; +struct timeval espera_deadline1; + +void scan_keyboard () { + char buf[256]; + struct timeval timeout = {0,0}; + fd_set rdset; + FD_ZERO (&rdset); + FD_SET (0, &rdset); + if (select (1, &rdset, NULL, NULL, &timeout) > 0) { + fgets (buf, 256, stdin); + if ((buf[0])!='\n'){ + switch (buf[0]) { + case 'a': + boton_alarma = 1; + printf("boton alarma = 1\n"); + break; + case 'b': + boton = 1; + printf("boton luz = 1\n"); + break; + case 'p': + presencia = 1; + printf("presencia = 1\n"); + break; + } + } + } +} + +static void task_principal (struct event_handler_t* this) { static const struct timeval period = { 1, 0 }; - static int cnt = 0; + fsm_fire (principal); + timeval_add (&this->next_activation, &this->next_activation, &period); +} - printf ("%d\n", cnt++); - +static void task_codigo_alarma (struct event_handler_t* this){ + static const struct timeval period = { 1, 0 }; + fsm_fire (codigo_alarma); timeval_add (&this->next_activation, &this->next_activation, &period); } +int main (){ + static struct timeval period = { 1, 0 }; + struct timeval next; -int -main () -{ - EventHandler eh1; + principal = fsm_new_principal(); + codigo_alarma = fsm_new_codigo_alarma(); + + printf("\n"); + printf("\t****************************************\n\n"); + printf("\tTeclas de activación:\n\n"); + printf("\t\tPresencia: p\n"); + printf("\t\tBotón luz: b\n"); + printf("\t\tPulsador código alarma: a\n"); + printf("\t\tContraseña de la alarma: 2 1 1\n\n"); + printf("\t****************************************\n\n"); + + EventHandler principal_eh, codigo_alarma_eh; reactor_init (); - event_handler_init (&eh1, 1, task1_func); - reactor_add_handler (&eh1); + event_handler_init (&principal_eh, 2, task_principal); + reactor_add_handler (&principal_eh); + + event_handler_init (&codigo_alarma_eh, 1, task_codigo_alarma); + reactor_add_handler (&codigo_alarma_eh); while (1) { - reactor_handle_events (); + timeval_add (&next, &next, &period); + scan_keyboard(); + reactor_handle_events(); } } diff --git a/reactor/reactor.c b/reactor/reactor.c index 917d184..7edcddf 100644 --- a/reactor/reactor.c +++ b/reactor/reactor.c @@ -1,7 +1,8 @@ #include "reactor.h" #include +#include "timeval_helper.h" -int +/*int timeval_less (const struct timeval* a, const struct timeval* b) { return (a->tv_sec == b->tv_sec)? (a->tv_usec < b->tv_usec) : @@ -30,7 +31,7 @@ timeval_sub (struct timeval* res, res->tv_sec --; res->tv_usec += 1000000; } -} +}*/ typedef struct reactor_t { diff --git a/reactor/reactor.h b/reactor/reactor.h index 303f0e2..bde9663 100644 --- a/reactor/reactor.h +++ b/reactor/reactor.h @@ -3,12 +3,12 @@ #include -int timeval_less (const struct timeval* a, const struct timeval* b); +/*int timeval_less (const struct timeval* a, const struct timeval* b); void timeval_add (struct timeval* res, const struct timeval* a, const struct timeval* b); void timeval_sub (struct timeval* res, const struct timeval* a, const struct timeval* b); - +*/ struct event_handler_t; typedef void (*eh_func_t) (struct event_handler_t*);