Redes de arcos constantes e coloridas. Demonstração com o PEP.

Verificação estrutural: cálculo de invariantes de lugar e armadilhas.

Exercícios sobre redes P/T: cálculo de grafos de acessibilidade e de cobertura, eliminação de contactos e arcos inibidores e verificação por enumeração de propriedades de segurança e animação.

Coloquei na página do projecto 5 duas ferramentas de edição de redes de Petri que usam como formato de gravação o PNML. Podem ser bastante úteis para os grupos que vão realizar esse projecto, mas quem não gostar do DaNAMiCS pode sempre experimentar uma destas ferramentas...

Verificação de propriedades de animação por enumeração. Verificação estrutural: matrizes de incidência e invariantes de lugar.

A lista dos projectos escolhidos até ao momento já está disponível. O projecto "P/T Nets em Haskell" já foi escolhido por dois grupos e, como tal, não aceito mais inscrições para este projecto. Relembro que os projectos estão dimensionados para grupos de dois elementos. Se o grupo for maior terá que realizar mais tarefas do que as especificadas.

Grafo de cobertura. Propriedades básicas de redes de Petri: finitude, animação, invertibilidade e exclusão mútua. Verificação por enumeração de propriedades de segurança.

Exercícios sobre modelação com redes P/T.

Especialmente para os amantes de XML, acabei de publicar um projecto sobre parsing e geração de PNML em Haskell. Já agora, gostava de referir que cada projecto só pode, no máximo, ser realizado por dois grupos (FIFO).

A partir da próxima semana a aula de Quarta-feira passa para as 11h00, mantendo-se no anfiteatro DI-A1.

Redes P/T: formalização, condição de activação e disparo e grafo de acessibilidade. Redes com capacidades explícitas e eliminação de contactos. Arcos inibidores.

Aplicações de redes elementares: exclusão mútua (incluindo algoritmo de Peterson) e protocolos (conversa cruzada).

Exercícios sobre redes elementares: cálculo de grafos de acessibilidade, detecção e eliminação de contactos, semântica não-entrelaçada e detecção de conflitos.

Noção de conflito, contacto e confusão. Cálculo do grafo de acessibilidade usando semântica entrelaçada e não-entrelaçada. Eliminação de contactos.

Já foram disponibilizados os primeiros enunciados de projectos práticos na secção de avaliação. Entretanto serão colocados mais enunciados com ênfase na programação em vez da modelação. Mal decidam o grupo e o projecto que pretendem realizar enviem-me um email.

Formalização do conceito de rede. Definição de rede simples e pura. Introdução às redes elementares: activação, disparo, e concorrência.

Introdução à ferramenta DaNAMiCS. Exercícios sobre modelação com redes elementares.

Introdução às redes de Petri.

Já podem encontrar no material de apoio os acetatos com a introdução à disciplina, e os acetatos sobre sistemas de transição.