eventb-rossi/eventb-skill

Desenvolvendo modelos Event-B

Um modelo Event-B é um sistema de transição discreto. Um CONTEXT contém conjuntos fixos, constantes e axiomas; uma MACHINE contém variáveis, invariantes e eventos guardados. Esta habilidade verifica o comportamento alcançável com o ProB e valida a boa definição. Ela não elabora provas interativas no Rodin.

1. Verificar as ferramentas necessárias

Requer rossi 0.1.8+ e eventb-animate 6.4+. Verifique-os; nunca instale ou atualize-os por conta própria. Se algum estiver ausente ou desatualizado, pare e peça ao usuário que o faça.

command -v rossi eventb-animate
rossi --version
eventb-animate --version

2. Escopo antes da modelagem

Escreva uma breve folha de requisitos no README.md do modelo:

• limite do sistema e exclusões explícitas;
• eventos observáveis e quem os executa;
• tipos de estado e as propriedades de segurança que devem sempre ser mantidas;
• um cenário de sucesso alcançável, um cenário proibido importante e se um estado terminal é intencional.

Para um modelo substancial ou qualquer refinamento de múltiplos níveis, adicione um registro de requisito-para-refinamento com uma linha por nível: cláusula de requisito/padrão, estado novo ou substituído, eventos afetados, invariante/relação de colagem e questão de validação. Divida um nível cuja linha contenha preocupações não relacionadas.

Use uma máquina por padrão; divida dados fixos em quantos contextos pequenos forem necessários para suas preocupações independentes. Adicione um nível de refinamento somente quando ele isolar um requisito distinto ou substituir uma representação de dados; escreva essa razão e o invariante de colagem primeiro. Refinamento é uma ferramenta, não uma cerimônia obrigatória.

Mantenha cada modelo em seu próprio diretório de projeto. Use um componente por arquivo, com o arquivo nomeado após o componente. Não coloque comentários em prosa em arquivos .eventb; mantenha a explicação no README.md.

3. Leia apenas a referência relevante

Necessidade	Leia
Gramática .eventb exata e formas de ação	references/syntax.md
Um operador ou sua precedência	references/math-toolkit.md
Ajuda para escolher estado, invariantes ou eventos	references/modelling.md
Uma etapa genuína de refinamento, ou planejamento de uma cadeia	references/refinement.md
Um padrão central de sistema reativo	o cabeçalho correspondente em references/patterns.md
Tempo discreto, prazos, modos ou sensores/atuadores	references/patterns-control.md
Múltiplos participantes: topologia, rodadas, consenso, canais, operações de longa duração	references/patterns-distributed.md
Controle de acesso, política de autorização ou reserva	references/patterns-security.md
Derivando um loop de uma pós-condição, ou um interpretador/ISA	references/patterns-algorithms.md
Solução de problemas de CLI ou um comando avançado condicional	references/tooling.md
Revisão final de design	references/best-practices.md

Comece de examples/counter/ apenas quando testemunhas ou refinamento de dados estiverem envolvidos; use examples/cars_on_bridge/ para divisão/convergência de eventos e examples/array_maximum/ para algoritmos de terminação. Não leia exemplos apenas para começar um pequeno modelo de máquina única.

4. Crie o menor modelo útil

• Coloque conjuntos de transporte e políticas/configurações fixas em um contexto.
• Digite cada variável com seu primeiro invariante, depois declare a regra de segurança real.
• Quando a detecção ou o controle cruzar um limite do sistema, mantenha o estado físico, reportado e comandado distintos e declare o atraso/incerteza permitido entre eles.
• Faça com que INITIALISATION estabeleça cada invariante.
• Dê a cada evento todas as guardas exigidas pelos requisitos funcionais e de transição, bem como pela preservação do invariante; as ações são executadas simultaneamente e as variáveis não atribuídas permanecem inalteradas.
• Represente um resultado importante no estado quando um objetivo de estado posterior deve observá-lo. Não adicione um evento sem efeito apenas para obter cobertura; um evento sem efeito habilitado muda o comportamento de deadlock e vivacidade.
• Mantenha os cenários de verificação finita pequenos. Parâmetros não determinísticos amplos multiplicam as habilitações de operação e podem tornar uma verificação, de outra forma finita, incompleta ou lenta.

5. Execute a verificação principal

Execute a partir do diretório do projeto do modelo, não de um pai contendo modelos não relacionados. Construa um .zip; ele contém os arquivos verificados que o animador precisa.

rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip

Aceite o resultado apenas quando:

• validação e construção não têm erros; trate missing or ill-typed witness e event is inaccurate como falhas mesmo que o comando saia com código zero;
• o relatório tem status: "ok" e nenhuma violação de invariante;
• não há deadlock inesperado; para um estado terminal deliberado, documente o predicado terminal e execute novamente com --no-deadlock em vez de afirmar liberdade de deadlock;
• o bloco Covered operations contém os eventos esperados (o relatório v3 não armazena cobertura de operação, então capture a saída do comando quando isso precisar ser auditado);
• completion.classification é complete para um cenário de aceitação finito;
• toda obrigação de boa definição é descarregada.

Um código de saída zero não é prova de completude. Se um modelo finito for relatado como incompleto, inspecione o motivo e os limites relevantes do ProB:

eventb-animate info --prefs /tmp/model.zip \
  | rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'

Aumente MAX_INITIALISATIONS ou MAX_OPERATIONS apenas o suficiente para enumerar as escolhas finitas conhecidas, então execute novamente e exija completion.classification: "complete". Para um modelo intencionalmente genérico/ilimitado, relate honestamente o resultado limitado e adicione um pequeno cenário finito separado quando uma verificação exaustiva for importante.

Se houver uma cadeia de refinamento, repita a verificação do modelo e wd para cada nível com -m <machine>.

6. Adicione evidência direcionada quando ela responder a uma pergunta

Use um rastreamento de meta quando a pergunta for se um predicado de estado é alcançável:

eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
  --save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip

Uma meta alcançada deliberadamente sai com código 1; exija uma repetição PERFECT. Em caso de falha de invariante ou deadlock, salve e repita seu contraexemplo antes de alterar o modelo.

Uma meta de estado não pode provar que um evento sem ação ou apenas com guarda foi disparado: ela pode parar assim que o estado de habilitação for alcançado. Confirme uma transição específica através do bloco Covered operations da verificação completa, ou direcione-a com geração de teste:

eventb-animate testgen -m M --operations EVENT_NAME \
  --out /tmp/scenario-traces /tmp/model.zip

Use estes apenas quando seu propósito mais restrito se aplicar:

• testgen: testemunhar uma transição específica ou gerar fixtures de operação reproduzíveis; não é uma verificação mais forte do que uma verificação exaustiva, e "não coberto" é inconclusivo.
• --symbolic ic3|kinduction: segurança de invariante ilimitada; não verifica deadlock, não relata cobertura de eventos nem fornece rastreamentos.
• po: verificar um projeto Rodin existente que já carrega provas .bpo/.bps.
• import/export: intercâmbio com Rodin, não o ciclo normal de autoria.

Consulte references/tooling.md para esses fluxos de trabalho condicionais. O backend padrão do ProB é o caminho normal de autoria.

7. Finalize com um artefato legível

Entregue os arquivos .eventb mais um breve README.md contendo escopo, forma do modelo, o invariante de segurança em linguagem simples, qualquer registro de refinamento, comandos de verificação exatos, completude, cobertura de eventos, resultado de WD e qualquer abstração deliberada. Uma execução limitada limpa significa “nenhum bug encontrado dentro do limite.” Uma execução finita completa prova apenas o comportamento alcançável verificado: ela ainda pode aceitar um invariante muito forte e não indutivo porque os estados violadores são inalcançáveis. Ela não descarrega obrigações de prova de invariante/refinamento do Event-B; apenas uma verificação de prova aplicável suporta essa afirmação. Consulte references/refinement.md, “verificação de modelo não é prova.”