Verificação 22/03/2012

   # # # # # # # # # # # # #
  # Verificação Automatica  #
  # Prof. Sérgio Campos     #
  # notasdogarcia.blog.com  #
   # # # # # # # # # # # # #

  Revisão:
  Quais estados levam a p?
  Inicialmente apenas p
  Na próxima interação, todos os que tem uma transição à p também levam a p.
  Isso é repetido até não ocorrerem mais alterações no grafo,
  indicando que não há mais novos elementos que levam a p.

  Vamos provar para um automato com dois programa em paralelo que se 1 está tentando (t1 = verdadeiro) então ele vai chegar em c1 (estado critico)

  t1 -> AF c1

  Temos de provar então que isso é verdade em todos os estados.
  Nos estados onde t1 é falso, isso é verdade por definiçào logica (se algo falso implica em alguma coisa necessariamente isso é verdade)
  Nos estados onde c1 é verdade t1 -> em c1, seja t1 verdade ou não.
  Nos estados que levam ao anterior t1 -> AF  c1 será verdade se todos os caminhos a partir daquele estado levarem ao conjunto de estados onde isso é verdade.

  note que é importante voce criar todas as possibilidades de estados.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  BDDs são bons spins não são intrinsicamente piores, são tão bons quanto.

  SAT é muito usado ultimamente.

  // Comentário solto: Existem 3 áreas de pesquisa maduras em computação hoje: Banco de Dados, SO e Compiladores.
  // E curiosamente raramente se vê artigos especificamente a respeito dessas areas. De fato voce ve esses artigos misturados com outras coisas.

 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

  // Vamos discutir o trabalho
  // Sugestão NUSMV que é a ferramenta que ele conhece e ele gosta dela, pode usar qualquer ferramenta madura.

  // O trabalho deve consistir em um exemplo não trivial.
  // No modelo escreva uma linha de cada vez e compile, porque uma única linha pode explodir seu modelo.

  // Escolha um programa que envolvesse paralelismo, que são os problemas mais interessantes.

  // há também um model checker feito pela turma do semestre passado, um segundo trabalho seria terminar ele.

  // assim temos 2 trabalhos 1 encontrar algo interesse pra fazer a checagem, e 2 terminar o model checker do semestre passado.