Conversão de P/T Nets para SMV
Considere a seguinte classe do Haskell que especifica uma rede P/T.
{-# OPTIONS -fglasgow-exts #-}
module PTNet where
import Data.Set
import Data.Map
class (Eq p, Show p, Eq t, Show t) => PTNet n p t where
places :: n p t -> Set p
trans :: n p t -> Set t
pre :: n p t -> Map (p,t) Int
pos :: n p t -> Map (t,p) Int
capacity :: n p t -> Map p Int
initial :: n p t -> Map p Int
Os tipos de dados Set e Map implementam, respectivamente, conjuntos e funções finitas e fazem parte das bibliotecas hierárquicas do GHC.
Neste projecto pretende-se que desenvolva uma função genérica que, dada uma rede, gere uma representação do seu grafo de acessibilidade usando lógica proposicional. O formato resultante deverá ser o mesmo aceite pela ferramenta de verificação simbólica SMV. Para que a tradução seja possível a rede deve ser limitada: a forma mais fácil de garantir esta propriedade consiste em exigir que todos os lugares tenham uma capacidade explícita. Se a rede for elementar devem ser utilizadas variáveis boleanas para representar os lugares.
Também deve ser implementada uma função que, dada uma rede com capacidades explícitas, gere uma rede equivalente livre de contactos. A tradução de uma rede livre de contactos para o SMV pode depois ser bastante simplificada.