- - - - CENAPAD-MGCO

A seguir: Sistemas de Transições de Acima: Modelos Formais: Progresso Anterior: Equidade fraca e equidade

Exemplo: Inteiro Oscilante

• Exemplo: considere o sistema abaixo, cujo estado é definido por uma única variável i, com valor inicial i=0
  

  Com Guarda Ação

  $$\gamma_{1}$$ i = 0 i := -1

  $$\gamma_{2}$$ i = -1 i = 0

  $$\gamma_{3}$$ i = 0 i = 1

  $$\gamma_{4}$$ i = 1 i = 0

  
  
  • Se este sistema obedece à hipótese de equidade fraca sobre $\gamma_{1}$, $\gamma_{2}$ e $\gamma_{3}$, então ele admite computações (infinitas) em que $\gamma_{3}$ nunca é executado;
  • se $\gamma_{1}$ e $\gamma_{2}$ são executados com equidade fraca, mas $\gamma_{3}$ é executado com equidade forte, então o sistema não admite computações em que $\gamma_{3}$nunca é executado.