Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • classic-prosa
  • wip-hunspell
  • prepare_MC_PR
  • tutorial
  • fset
  • embed_arr_seq_uniq
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
Compare
Björn Brandenburg's avatar
do the big rt->prosa move
Björn Brandenburg authored 
Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.
0d8c78ae
History
Björn Brandenburg's avatar 0d8c78ae
History
Name Last commit Last update
..
README.md
all.v
arrival_sequence.v
job.v
ready.v
schedule.v
service.v
time.v
README.md

Prosa Behavior Specification

This module defines the Prosa trace-based semantics. The following rules/guidelines apply to this module:

  • Files in this module must be largely self-contained and may depend only on "helper" definitions in rt.util. In particular, nothing in here may depend on concepts in the model or analysis modules.

  • This module is purely a specification of semantics. There are no proofs.

  • This behavior specification strives to be (almost) minimal. If a concept doesn't have to be defined here, if it is not required to state the basic trace semantics, then it should be introduced elsewhere.

  • The behavior specification is the universally agreed-upon foundation of Prosa. Everyone uses this; there are no alternatives to the basic definitions introduced here.

  • If there are multiple competing sets of assumptions in the literature, then that's a sure sign that it should go into the model or analysis modules.

  • Changes here are extremely sensitive precisely because this is the part of the library that everyone is going to use, so significant changes here should be discussed early and extensively.