br.uerj.petrinetanalyzer.engine
Class PetriNetAnalyzer

java.lang.Object
  br.uerj.petrinetanalyzer.engine.PetriNetAnalyzer

All Implemented Interfaces:

IntfEngineConstants

public class PetriNetAnalyzer
extends java.lang.Object
implements IntfEngineConstants

Classe que cuida da engine da Análise da Rede de Petri

Author:

Felipe Lino
Data: 25/02/2007
Atualizado: 12/10/2007

Field Summary

private PetriNetProperties	properties Propriedades da Rede
private javax.swing.tree.DefaultMutableTreeNode	root Nó raíz da árvore de alcançabilidade
private ImplSimulator	simulator Engine do Simulador
private javax.swing.JTree	tree Árvore de alcançabilidade
private javax.swing.tree.DefaultTreeModel	treeModel Model usado para tratar a árvore de alcançabilidade, apenas prepara a árvore para ser usada na interface gráfica.

Fields inherited from interface br.uerj.petrinetanalyzer.common.interfaces.IntfEngineConstants

ERROR_CODE, STATE_DUPLICADO, STATE_FRONTEIRA, STATE_INTERIOR, STATE_TERMINAL, TOKEN_INFINITO

Constructor Summary

PetriNetAnalyzer(ImplPetriNetBase pn)
Construtor que recebe a Rede de Petri como Parâmetro.

Method Summary

javax.swing.tree.DefaultMutableTreeNode	addObject(javax.swing.tree.DefaultMutableTreeNode parent, java.lang.Object child) Adiciona um novo nó na árvore de seqüência de disparos.
static int	compareMarking(PetriNetState stateA, PetriNetState stateB) Método que compara a marcação de 2 estados recebidos como parâmetro.
PetriNetState	createNewState(javax.swing.tree.DefaultMutableTreeNode nodeX, int transicao) Cria um Novo Estado para a árvore de alcançabilidade.
void	geraArvore(javax.swing.tree.DefaultMutableTreeNode node) Função recursiva, que vai varrendo a árvore que vai sendo criada, e processando seus nós.
void	geraArvoreAlcancabilidade() Gera a arvore de alcançabilidade da Rede de Petri e verifica propriedades.
PetriNetProperties	getProperties() Retorna as Propriedades encontradas na Rede.
javax.swing.JTree	getTree() Retorna a Árvore de Alcançabilidade.
void	processNode(javax.swing.tree.DefaultMutableTreeNode nodeX) Processa o Nó da árvore de alcançabilidade Algoritmo: Seja o X o nó a ser processado. 1) Se existe um nó Y na árvore que não é fronteira e tem a mesma marcação que X.
void	verifyConservativa(PetriNetState stateX) Uma Rede é conservativa se o total de fichas na rede se mantém.
void	verifyLimite(PetriNetState stateX) Uma rede é limitada, se para todas as marcações acessíveis, o número de fichas em qualquer lugar da Rede não exceder K (inteiro - limite).
void	verifyProperties(PetriNetState stateX) Verifica várias propriedades da Rede de Petri.
void	verifyVivacidade(PetriNetState stateX) Uma rede é viva se pelo menos uma transição puder ser disparada, em qualquer estado, ou seja ela é morta, se chegar a algum estado que não tenha transições para disparar.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

simulator

private ImplSimulator simulator

Engine do Simulador

properties

private PetriNetProperties properties

Propriedades da Rede

tree

private javax.swing.JTree tree

Árvore de alcançabilidade

root

private javax.swing.tree.DefaultMutableTreeNode root

Nó raíz da árvore de alcançabilidade

treeModel

private javax.swing.tree.DefaultTreeModel treeModel

Model usado para tratar a árvore de alcançabilidade, apenas prepara a árvore para ser usada na interface gráfica.

Constructor Detail

PetriNetAnalyzer

public PetriNetAnalyzer(ImplPetriNetBase pn)

Construtor que recebe a Rede de Petri como Parâmetro.

Parameters:

pn - Rede de Petri a ser analizada

Method Detail

geraArvoreAlcancabilidade

public void geraArvoreAlcancabilidade()

Gera a arvore de alcançabilidade da Rede de Petri e verifica propriedades.

 Algoritmo: 
  root = Estado Inicial;
  processNode(root);
  verifyProperties(root);
  geraArvore(root);
 

geraArvore

public void geraArvore(javax.swing.tree.DefaultMutableTreeNode node)

Função recursiva, que vai varrendo a árvore que vai sendo criada, e processando seus nós.

 Algoritmo: Seja N o nó recebido como parâmetro.
  Para i de 1 até Número de filhos de N Faça
     X = N.getFilho(i);
     processNode(X);
     geraArvore(X);
     verifyProperties(X);
  Fim Para
 

Parameters:

node - Nó pai, cujos filhos serão processados.

processNode

public void processNode(javax.swing.tree.DefaultMutableTreeNode nodeX)

Processa o Nó da árvore de alcançabilidade

 Algoritmo:
 Seja o X o nó a ser processado.
 1) Se existe um nó Y na árvore que não é fronteira e tem a mesma marcação que X.
    então X é um nó DUPLICADO.

   Para cada nó Y da arvore Faça
      Se ((µ(Y) = µ(X)) E (Y != X) E (Y.tipo != FRONTEIRA)) Então 
         X.tipo = DUPLICADO; 
         retorna;
      Fim Se
   Fim Para.
 
 2) Se não existem transições sensibilizadas associadas à marcação µ(x),
 ou seja {d (µ(x),tj) é indefinida PARA todo tj pertencente à T};
 então X é um nó TERMINAL.
  
   Se (X.temTransicaoDisponivel == false) Então
      X.tipo = TERMINAL;
      retorna;
   Fim Se
    
 3) Para todas as transições tj Pertencente à T, que são habilitadas em µ[x],
 cria-se um novo nó Z, na árvore de alcançabilidade, ligados ao primeiro,
 através de um arco ao qual se associa a transição disparada.
 
 Um arco, designado tj é dirigido do nó X para o nó Z. O nó X é redefinido como nó INTERIOR
 e Z, torna-se um nó FRONTEIRA.

  Para cada transição habilitada  T de X Faça
     Z = createNewState(X);
     Z.tipo = FRONTEIRA;
     AdicionaNóNaArvore(Z);
  Fim Para
  X.tipo = INTERIOR;

 

createNewState

public PetriNetState createNewState(javax.swing.tree.DefaultMutableTreeNode nodeX,
                                    int transicao)

Cria um Novo Estado para a árvore de alcançabilidade.
A marcação do novo estado criado, estado Z, segue a seguinte regra:
Inicialmente marcação de Z é o resultado do disparo da transição tj a partir do estado X.
Se existe um nó Y no percurso da raiz até X cuja marcação de Z seja superior à marcação resultante do disparo da transição isto é:
µ[z] > µ[y] e µ[z]i > µ[y]i, Então µ[z]i = w.
O símbolo 'w' representa um crescimento de fichas em determinado lugar da rede.

 Algoritmo: Seja X o pai de Z na árvore, e Z o nó a ser processado.
 Z = Disparo de Tj a partir de X;
 Y = X;
 Enquanto ( Y <> null ) Faça
   Se Marcacao(Z) > Marcacao(Y) Então
     Para i de 1 até total de lugares Faça
       Se (Z.lugar[i].fichas > Y.lugar[i].fichas) Então
         Z.lugar[i].fichas = w;
     Fim Para
   Fim Se
                
   Y = Y.getPai();
                
 Fim Enquanto

 retorna Z;
 

Parameters:

nodeX - Nó pai

transicao - Número da transição disparada

Returns:

Estado após disparo da transição.

compareMarking

public static int compareMarking(PetriNetState stateA,
                                 PetriNetState stateB)

Método que compara a marcação de 2 estados recebidos como parâmetro.

• Se marcação do estado A > Marcação do estado B retorna +1
• Se marcação do estado A = Marcação do estado B retorna 0
• Se marcação do estado A < Marcação do estado B retorna -1

 Algoritmo: ComparaMarcacao(A,B) <--> [Marcacao(A) > Marcacao(B)]

 boolean existe = false;  // Existe um lugar de A que possui fichas > Lugar de B
 boolean maior  = true;   // Todo lugar de A possui fichas > Todo Lugar de B

 Para i de 1 até numero de lugares Faça:
    Se (A.lugar[i].fichas >= B.lugar[i].fichas) E (maior = true)Então
       maior = true;
       Se (A.lugar[i].fichas > B.lugar[i].fichas) 
           existe = true;
    Senão
       maior = false;
    Fim Se
 Fim Para

 Se ( maior = true ) E ( existe = true) Então
    retorna 1;
 Se ( maior = true ) E ( existe = false ) Então
    retorna 0;
 Se (maior = false) Então
    retorna -1;
 

Parameters:

stateA - Estado A

stateB - Estado B

Returns:

resultado da comparação.

addObject

public javax.swing.tree.DefaultMutableTreeNode addObject(javax.swing.tree.DefaultMutableTreeNode parent,
                                                         java.lang.Object child)

Adiciona um novo nó na árvore de seqüência de disparos.

Parameters:

parent - Nó pai

child - Estado filho

Returns:

Nó criado

verifyProperties

public void verifyProperties(PetriNetState stateX)

Verifica várias propriedades da Rede de Petri.

1. Limitação
2. Conservação
3. Vivacidade

Parameters:

stateX - Estado a ser verificado

verifyLimite

public void verifyLimite(PetriNetState stateX)

Uma rede é limitada, se para todas as marcações acessíveis, o número de fichas em qualquer lugar da Rede não exceder K (inteiro - limite). O algoritmo parte do princípio que ela é limitada. Se ela em algum momento deixar de ser limitada, ele pára de testar qual o limite. É ilimitada quando for encontrado em algum Lugar um número infinito de fichas (w).

Parameters:

stateX - Estado a ser verificado.

verifyConservativa

public void verifyConservativa(PetriNetState stateX)

Uma Rede é conservativa se o total de fichas na rede se mantém. O algoritmo parte do princípio que a rede é conservativa, se ela deixar de ser conservativa ele pára de fazer o teste.

Parameters:

stateX - Estado a ser verificado.

verifyVivacidade

public void verifyVivacidade(PetriNetState stateX)

Uma rede é viva se pelo menos uma transição puder ser disparada, em qualquer estado, ou seja ela é morta, se chegar a algum estado que não tenha transições para disparar.

Parameters:

stateX - Estado a ser verificado.

getTree

public javax.swing.JTree getTree()

Retorna a Árvore de Alcançabilidade.

Returns:

Árvore de Alcançabilidade

getProperties

public PetriNetProperties getProperties()

Retorna as Propriedades encontradas na Rede.

Returns:

Propriedades da Rede de Petri.