-
Notifications
You must be signed in to change notification settings - Fork 2
Model Checking Intermediate Language
The Model Checking Intermediate Language (MoChIL, for short) is an intermediate language meant to be a common input and output standard for model checker for finite- and infinite-state systems, with an initial focus is on finite-state ones.
MoChIL has been designed to be general enough to be a target language for a variety of user-facing model specification languages.
For being an intermediate language, its models are meant to be produced and processed by tools, hence it was designed to have
- simple, easily parsable syntax
- minimal syntactic sugar, at least initially
- simple semantics
- a small but comprehensive set of commands
- simple translations to lower level modeling languages such as Btor2 and Aiger.
Based on these principles, MoChIL provides no direct support for many of the features offered by current hardware modeling languages such as VHDL and Verilog or more general purpose system modeling languages such as SMV, TLA+, PROMELA, Simulink, SCADE, Lustre. However, it strives to offer enough capability so that problems expressed in those languages can be reduced to problems in MoChIL.
MoChIL is an extension the SMT-LIB language with new commands to define and verify systems. It allows the definition of multi-component synchronous reactive systems. It also allows the specification and checking of state invariants, transition invariants and deadlocks, possibly under fairness conditions on input values.
MoChIL assumes a linear notion of time and hence has a standard trace-based semantics.
Each system definition:
- is parametrized by a state signature, a sequence of sorted variables;
- divides state variables into input, output and local variables;
- it defines a transition systems via the formalization of an initial state predicate and a transition predicate from (many-sorted) FOL;
- can be expressed as the synchronous or asynchronous composition of other systems
Notation: If an FOL F is a formula and x a tuple of distinct variables, let F[x] express the fact that every variable in x is free in F.
Formally, a transition system S is a pair of predicates of the form
S = ( λ i:δ λ o:τ IS [i, o, s], λ i:δ λ i':δ λ o:τ λ o':τ TS [i,o,s,i',o',s'] )
where
-
i = (i1, ..., im) and i' = (i1', ..., im') are two tuples of input variables, both of type δ = (δ1, ..., δm)
-
s = (s1, ..., sp) and s' = (s1', ..., sp') are two tuples of local (or, internal state) variables, both of type σ = (σ1, ..., σp)
-
o = (o1, ..., on) and o' = (o1', ..., on') are two tuples of output variables, both of type τ = (τ1, ..., τn)
-
IS [i, o, s] is the system's initial state condition, expressed as an SMT-LIB formula over the input variables i, output variables o and local variables s.
-
TS [i, o, s, i', o', s'] is the system's transition relation, expressed as an SMT-LIB formula over the current-state input (i), output (o), and local (s) variables, and next-state next-state input (i'), output (o'), and local (s') variables.
Note: Similarly to Mealy machines, the initial state condition is also meant to specify the initial system's output based on the initial state and input. Correspondingly, the transition relation is also meant to specify the system's output in every later state of the computation.
Note: The input and output values corresponding to the transition to the new state are those in the variables i' and o'. The values of i, o are the old input and output values.
Note: In this formulation, for uniformity, input and output variables are automatically stateful since the transition relation formula can access old values of inputs and outputs in addition to the old values of the local state. This means that, technically, S is a closed system. The designation of some state variables as input or output is, however, important when combining systems together, to capture which of the state values are shared between two systems being combined, and how.
SMT-LIB is a command-based language with LISP-like syntax designed to be a common input/output language for SMT solvers.
MoChIL adopts the following SMT-LIB commands:
-
(declare-sort s n)
Declares s to be a sort symbol (i.e., type constructor) of arity n. Examples:
(declare-sort A 0) (declare-sort Set 1) ; possible sorts: A, (Set A), (Set (Set A)), ...
-
(define-sort s (u1 ⋅⋅⋅ un) τ)
Defines s as synonym of a parametric type τ with parameters u1 ⋅⋅⋅ un. Examples:
(declare-sort NestedSet (X) (Set (Set X))) ; possible sorts: (NestedSet A), ... -
(declare-const c σ)
Declares a constant c of sort σ. Examples:
(declare-const a A) (declare-const n Int)
-
(define-fun f ((x1 σ1) ··· (xn σn)) σ t)
Defines a (non-recursive) function f with inputs x1, ..., xn (of respective sort σ1, ..., σn), output sort σ, and body t.
-
(set-logic L)
Defines the model's data logic, that is, the background theories of relevant datatypes (e.g., integers, reals, bit vectors, and so on) as well as the language of allowed logical constraints (e.g., quantifier-free, linear, etc.).
One addition to SMT-LIB is the binary symbol != for disequality.
For each term s and t of the same sort, (!= s t) has the same meaning as (not (= s t)) or, equivalently, (distinct s t).
(declare-enum-sort s (c1 ⋅⋅⋅ cn))
Declares s to be an enumerative type with (distinct) values c1, ..., cn.
(define-system S
:input ((i1 δ1) ⋅⋅⋅ (im δm))
:output ((o1 τ1) ⋅⋅⋅ (on τn))
:local ((s1 σ1) ⋅⋅⋅ (sp σp))
:init (I1 ⋅⋅⋅ Iq)
:trans (T1 ⋅⋅⋅ Tr)
:inv (P1 ⋅⋅⋅ Ps)
)
where
- S is the system's identifier;
- each ij is an input variable of sort δj;
- each oj is an output variable of sort τj;
- each sj is a local variable of sort σj;
- each ij, oj, sj denote current-state values
- next-state variables are not provided explicitly but are denoted by convention appending ' to the names of the current-state variables ij, oj, and sj;
- each Ij is an SMT-LIB formula over the input, output and current-state variables or a system application that expresses a constraint on the initial states of S;
- each Tj is an SMT-LIB formula over all of the system's variables or a system application that expresses a constraint on the state transitions of S;
- each Pj is an SMT-LIB formula over all of the unprimed system's variables that expresses a constraint on all reachable states of S;
- a system application has the form (Si xi1 ⋅⋅⋅ xim yi1 ⋅⋅⋅ yin) where Si is a system other than S with im inputs and in outputs, and each x is a variable of S and each y is a local or output variable of S.
The various aspects of the system are provided as SMT-LIB attribute-value pairs. The order of the attributes can be arbitrary but each attribute can occur at most once. A missing attribute stands for a default value: the empty list (). The sequence of formulas in the :init (resp., :trans and :inv) attribute is to be understood conjunctively.
Formally, the system S specified with a define-system is the pair
S = ( λi:δ λo:τ IS[i,o,s], λi:δ λi':δ λo:τ λo':τ TS[i,o,s,i',o',s'] )
defining a transitions system with initial state condition IS and transition relation TS where
-
IS = I1 ∧ ⋅⋅⋅ ∧ Iq ∧ P1 ∧ ⋅⋅⋅ ∧ Ps;
-
TS = T1 ∧ ⋅⋅⋅ ∧ Tr ∧ (P1 ∧ ⋅⋅⋅ ∧ Ps )[i ↦ i', o ↦ o', s ↦ s'];
-
If Ii is the application (Si xi yi), it is syntactic sugar for the formula fresh(fst(Si) xi yi);
-
If Ti is the application (Si xi yi), it is syntactic sugar for the formula fresh(snd(Si) xi x'i yi y'i);
-
fst in the first projection over pairs and snd is the second;
-
for any formula F, the expression fresh(F) denotes the formula obtained from F by replacing each free variable of F by a fresh variable.
Notes:
-
The full set s of local variables of S is (recursively) the disjoint union of the variables declared in the :local attribute together with the local variables of all the systems applied in :init or :trans.
-
The order of the formulas in :init, :trans and :inv attributes does not matter.
-
TS is not required to be functional over inputs and current state, thus allowing the modeling of non-deterministic systems.
Let's extend the syntax and the semantics of (first-order) LTL to allow primed stated variables in formulas, interpreting them over a trace as the value they have in the second state of the trace.
Then, the set of traces defined by the transition system (IS, TS) is exactly the set of traces that satisfy the LTL formula: IS[i,o,s] ∧ always TS[i,o,s,i',o',s'].
Discussion: Should we restrict the semantics to infinite traces only?
Since it is possible to define systems that have deadlock states (reachable states with no successors, more precisely, reachable states falsifying the transition constraints), finite traces ending in a deadlock state have to be excluded from the semantics. In that case though, it is not possible to disprove safety properties by means of a finite counterexample trace because that trace may not extend to an infinite trace of the system.
In contrast, allowing finite traces as well in the semantics has the problem that ...
One way to address the deadlock state problem is to consider only infinite traces in the semantics (systems that are meant to reach a final state can be always modeled with states that cycle back to themselves and produce stuttering outputs). In that semantics, the reachability of a deadlock state (a state with no successors in the transition relation) indicates an error in the system's definition.
Intuitively, for a system definition to define a system with no deadlocks:
-
Any assignment of values to the input variables can be extended to a total assignment (to all the unprimed variables) that satisfies IS.
-
For any reachable state s, any assignment to the primed input variables can be extended to a total assignment s' so that s,s' satisfies TS.
The first restriction above guarantees that the system can start at all. The second ensures that from any reachable state and for any new input the system can move to another state (and so also produce output).
-
A sufficient condition for (1) is that the following formula is valid in the (previously specified) background theory: ∀ i ∃ o ∃ s IS
-
A sufficient condition for (2) is that the following formula is valid in the background theory: ∀ i ∀ o ∀ s ∀ i' ∃ o' ∃ s' TS
This condition is not necessary, however, since it need not apply to unreachable states. Let Reachable[i, o, s] denote the (possibly higher-order) formula satisfied exactly by the reachable states of S. Then, a more accurate sufficient condition for (2) above would be the validity of the formula:
∀ i ∀ o ∀ s ∀ i' ∃ o' ∃ s' (Reachable[i,o,s] ⇒ TS)
Note: In general, checking the two sufficient conditions above automatically can be impossible or very expensive (because of the quantifier alternations in the conditions).
(Adapted from "Principles of Cyber-Physical Systems" by R. Alur, 2015)
Note: When reading these examples, it is helpful to keep in mind that, intuitively, in the :init formulas the input values are given and the local and output values are to be defined with respect to them. In contrast, in the :trans formulas the new input values, and old input, output and local values are given, and the new local and output values are to be defined.
; The output of Delay is initially 0 and then is the previous input.
; No local variable is needed
(define-system Delay
:input ( (in Int) )
:output ( (out Int) )
:init (
(= out 0)
)
:trans (
; the new output is the old input
(= out' in)
)
)
; The output of Delay2 is initially any number in [0,10] and then is its previous input.
(define-system Delay2
:input ( (in Int) )
:output ( (out Int) )
:init (
(<= 0 out 10) ; more than one possible initial output
)
:trans (
(= out' in)
)
)
(define-enum-sort LightStatus (on off))
; TimedSwitch models a timed light switch where the light stays
; on for at most 10 steps unless it is switched off before.
; The input Boolean is interpreted as an on or off command
; depending on whether the light was respectively off or on.
; set-of-transitions-style definition
(define-system TimedSwitch1
:input ( (press Bool) )
:output ( (sig Bool) )
:local ( (status LightStatus) (n Int) )
:init (
(= n 0)
(ite press (= status on) (= status off))
(= sig (= status on))
)
:trans (
(= sig' (= status' on))
(let ((stay-off (and (= status off) (not press') (= status' off) (= n' n)))
(turn-on (and (= status off) press' (= status' on) (= n' n)))
(stay-on (and (= status on) (not press') (< n 10) (= status' on) (= n' (+ n 1))))
(turn-off (and (= status on) (or press' (>= n 10)) (= status' off) (= n' 0)))
)
(or stay-off turn-on turn-off stay-on)
)
)
)
; guarded-transitions-style definition
(define-system TimedSwitch2
:input ( (press Bool) )
:output ( (sig Bool) )
:local ( (status LightStatus) (n Int) )
:init (
(= n 0)
(ite press (= status on) (status off))
(= sig (= status on))
)
:trans (
(= sig' (= status' on))
(=> (and (= status off) (not press'))
(and (= status' off) (= n' n)))
(=> (and (= status off) press')
(and (= status' on) (= n' n)))
(=> (and (= status on) (not press') (< 10 n))
(and (= status' on) (= n' (+ n 1))))
(=> (and (= status on) (or press' (>= n 10)))
(and (= status' off) (= n' 0)))
)
)
(define-fun flip ((s LightStatus)) LightStatus
(ite (= s off) on off)
)
; equational-style definition
(define-system TimedSwitch3
:input ( (press Bool) )
:output ( (sig Bool) )
:local ( (status LightStatus) (n Int) )
:init (
(= n 0)
(= status (ite press on off))
(= sig (= status on))
)
:trans (
(= sig (= status' on))
(= status' (ite press' (flip status)
(ite (= status off) off
(ite (< n 10) on off))))
(= n' (ite (or (= status off) (status' off)) 0
(+ n 1)))
)
)
; `NonDetArbiter` grants input requests expressed by the (Boolean) event `req1` and `req2`.
; Initially, no requests are granted. Afterwards, a request is always granted (expressed
; by issuing the event `gran1` or `grant2`), if it is the only request.
; When both inputs contain a request, one of the two is granted, with a non-deterministic
; choice.
;
(define-system NonDetArbiter
:input ( (req1 Bool) (req2 Bool) )
:output ( (gran1 Bool) (gran2 Bool) )
:local ( (s Bool) )
:init ( (not gran1) (not gran2) ) ; nothing is granted initially
:trans (
(=> (and (not req1') (not req2'))
(and (not gran1') (not gran2')))
(=> (and req1' (not req2'))
(and 'gran1 (not gran2')))
(=> (and (not req1') req2')
(and (not gran1') gran2'))
(=> (and req1' req2')
; the unconstrained value of `s` is used as non-deterministic choice
(ite s'
(and gran1' (not gran2')
(and (not gran1') gran2'))))
)
)
; `DelayedArbiter` is similar to `NonDetArbiter` but grants requests a cycle later.
(define-system DelayedArbiter
:input ( (req1 Bool) (req2 Bool) )
:output ( (gran1 Bool) (gran2 Bool) )
:local ( (s Bool) )
:init ( (not gran1) (not gran2) ) ; nothing is granted initially
:trans (
(=> (and (not req1) (not req2))
(and (not gran1') (not gran2')))
(=> (and req1 (not req2))
(and gran1' (not gran2')))
(=> (and (not req1) req2)
(and (not gran1') gran2'))
(=> (and req1 req2)
; the unconstrained value of `s` is used as non-deterministic choice
(ite s
(and gran1' (not gran2')
(and (not gran1') gran2'))))
)
)
; Events carrying data can be modeled as instances of the polymorphic algebraic datatype
; (Event X) where X is the type of the data carried by the event.
(declare-datatype Event (par (X)
(none)
(some (val X))
))
; Similar to `NonDetArbiter` but for requests expressed as integer events.
(define-system IntNonDetArbiter
:input ( (req1 (Event Int)) (req2 (Event Int)) )
:output ( (gran1 (Event Int)) (gran2 (Event Int)) )
:local ( (s Bool) )
:init ( (= gran1 gran2 none) )
:trans (
(=> (= req1' req2' none)
(= gran1' gran2' none))
(=> (and (distinct req1' none) (= req2' none))
(and (= gran1' req1) (= gran2' none)))
(=> (and (= req1' none) (distinct' req2' none))
(and (= gran1' none) (= gran2' req2')))
(=> (and (distinct req1' none) (distinct req2' none))
(ite s
(and (= gran1' req1') (= gran2' none))
(and (= gran1' none) (= gran2' req2'))))
)
)
; An event-triggered channel that arbitrarily loses its input data
(define-system LossyIntChannel
:input ( (in (Event Int)) )
:output ( (out (Event Int)) )
:local ( (s Bool) )
; whether the input event is transmitted depends on s
; s is unconstrained so can take any value during execution
:inv ( (= out (ite s in none)) )
)
; A system that simply passes along the current input `in` when the `clock` input is true.
; When `clock` is false it outputs the value output the last time `clock` was true.
; Until `clock` is true for the first time it outputs the initial value of `init`.
(define-system StutteringClockedCopy
:input ( (clock Bool) (init Int) (in Int) )
:output ( (out Int) )
:init ( (ite clock (= out s in) (= out s init)) )
:trans ( (ite clock (= out' s' in) (= out' s' s)) )
)Parallel composition is achieved by applying systems in initial state or transition conditions.
;----------------
; Two-step delay
;----------------
; +------------------------------------+
; | DoubleDelay |
; | +-----------+ +-----------+ |
; in | | | temp | | | out
; ----+->| Delay |----->| Delay |--+---->
; | | | | | |
; | +-----------+ +-----------+ |
; +------------------------------------+
; One-step delay
(define-system Delay
:input ( (i Int) )
:output ( (o Int) )
:init ( (= o 0) )
:trans ( (= o' i) )
)
; Two-step delay
(define-system DoubleDelay
:input ( (in Int) )
:output ( (out Int) )
:local ( (temp Int) )
:init ( (Delay in temp) ; can be understood as a macro call that also adds state
(Delay temp out) )
:trans ( (Delay in temp)
(Delay temp out) )
)
;; DoubleDelay expanded
(define-system DoubleDelay
:input ( (in Int) )
:output ( (out Int) )
:local ( (temp Int) )
:init ( (= temp 0) ; expansion of `(Delay in temp)`
(= out 0) ; expansion of `(Delay temp out)`
)
)
:trans ( (= temp' in) ; expansion of `(Delay in temp)`
(= out' temp) ; expansion of `(Delay temp out)`
)
)
; Example trace:
; in = 1, 2, 3, 4, 5, 6, 7, ...
; temp = 0, 1, 2, 3, 4, 5, 6, ...
; out = 0, 0, 1, 2, 3, 4, 5, ...
; 'Latch' has a Boolean state represented by state variable `s` with arbitrary initial value.
; A set request (represented by input `set` being true) sets the new value of `s` to true
; unless there is a concurrent reset request (represented by input `reset` being true).
; In that case, the choice between the two requests is resolved arbitrarily.
; In the absence of either a set or a reset, the value of `s` is unchanged.
; The initial value of output 'out' is arbitrary. Afterwards, it is the previous value of 's'.
;
(define-system Latch
:input ( (set Bool) (reset Bool) )
:output ( (out Bool) )
:local ( (s Bool) )
:trans (
(= out' s)
(=> (and (not set) (not reset)) (= s' s))
(=> (and set (not reset)) (= s' true))
(=> (and (not set) reset) (= s' false))
; when the old values of `set` and `reset` are both `true`,
; the new value of `s` is arbitrary
)
)
; More compact, equational definition of Latch
(define-system Latch1
:input ( (set Bool) (reset Bool) )
:output ( (out Bool) )
:local ( (b Bool) ) ; used for non-deterministic choice
:trans (
(= out' (or (and set (or (not reset) b))
(and (not set) (not reset) out)))
)
)
;---------------
; 3-bit counter
;---------------
; 'OneBitCounter' is a stateful 1-bit counter implemented using
; the latch component modeled by `Latch`.
; The counter goes from 0 (represented as `false`) to 1 (`true`)
; with a carry value of 0, or from 1 to 0 with a carry value of 1 when
; the increment signal `inc` is true.
; It is reset to 0 (`false`) when the start signal is true.
; The initial value of the counter is arbitrary.
; +------------------------------------------------------------+
; | |
; | +--------------------------------------------------------+ |
; | | +-------+ | |
; +-|-----------------------------------|``-. set | | | |
; | | |`-._ | :---->| | | |
; | +->|``-. +--| _]o--|..-` | Latch | | |
; | | :--+----\``-. | |.-` reset | |-+-+--> out
; inc -+----|..-` | ) :--+--------------------->| | |
; | | +--/..-` +-------+ |
; | | | |
; start ----------------+ OneBitCounter |
; | | |
; +------------+-----------------------------------------------+
; |
; v carry
(define-system OneBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (out Bool) (carry Bool) )
:local ( (set Bool) (reset Bool) )
:init (
(Latch set reset out)
(= set (and inc (not reset)))
(= reset (or carry start))
(= carry (and inc out))
)
:trans (
(Latch set reset out)
(= set' (and inc' (not reset')))
(= reset' (or carry' start'))
(= carry' (and inc' out'))
)
)
; a more concise version
(define-system OneBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (out Bool) (carry Bool) )
:local ( (set Bool) (reset Bool) )
:inv (
; _one-state_ constraints asserted for every state
(= set (and inc (not reset)))
(= reset (or carry start))
(= carry (and inc out))
)
:init (
(Latch set reset out)
)
:trans (
(Latch set reset out)
)
)
; an even more concise version
(define-system OneBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (out Bool) (carry Bool) )
:local ( (set Bool) (reset Bool) )
:inv (
; _one-state_ constraints asserted for every state
(= set (and inc (not reset)))
(= reset (or carry start))
(= carry (and inc out))
)
:compose ( ; new attribute
; application below is implicitly added to both :init and :trans
(Latch set reset out)
)
)
; 'ThreeBitCounter' implements a 3-bit resettable counter
; by cascading three 1-bit counters.
; The output is three Boolean values standing for the three bits,
; with out0 being the least significant one.
;
(define-system ThreeBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (out0 Bool) (out1 Bool) (out2 Bool) )
:local ( (car0 Bool) (car1 Bool) (car2 Bool) )
:init (
(OneBitCounter inc start out0 car0)
(OneBitCounter car0 start out1 car1)
(OneBitCounter car1 start out2 car2)
)
:trans (
(OneBitCounter inc start out0 car0)
(OneBitCounter car0 start out1 car1)
(OneBitCounter car1 start out2 car2)
)
)
; more concisely
define-system ThreeBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (out0 Bool) (out1 Bool) (out2 Bool) )
:local ( (car0 Bool) (car1 Bool) (car2 Bool) )
:compose (
(OneBitCounter inc start out0 car0)
(OneBitCounter car0 start out1 car1)
(OneBitCounter car1 start out2 car2)
)
)
(check-system S :input ((i1 δ1) ⋅⋅⋅ (im δm)) :output ((o1 τ1) ⋅⋅⋅ (on τn)) :local ((s1 σ1) ⋅⋅⋅ (sp σp)) :assumptions (a1 ⋅⋅⋅ aq) :fairness (f1 ⋅⋅⋅ fh) :reachable (r1 ⋅⋅⋅ ri) :invariants (p1 ⋅⋅⋅ pk) )
where
- S is the identifier of a previously defined system with m inputs, n outputs, and p local variables;
- each ij is a renaming of the corresponding input variable of S of sort δi;
- each oj is a renaming of the corresponding output variable of S of sort τi;
- each sj is a renaming of the corresponding local variable of S of sort σi;
- each aj is a triple of the form (nj lj Aj)
with Aj a formula over input and local variables (called environmental assumption); - each fj is a triple of the form (nj lj Fj) with Fj a formula over input, output and local variables (called fairness condition);
- each rj is a triple of the form (nj lj Rj) where Rj is a formula over input, output and local variables (called reachability condition);
- each pj is a triple of the form (nj lj Pj) where Pj is a formula over input, output and local variables (called invariance condition);
- each nj is fresh identifier
- each lj is a string literal
- a formula is an (quantifier-free?) FOL formula over primed and unprimed variables
Note: The ids nj are meant to be user-defined names for the corresponding condition. The strings nj are labels that can be attached for convenience, especially when producing output.
Let IS and TS be respectively the initial state condition and transition predicate of S.
Let A = A1 ∧ ⋅⋅⋅ ∧ Aq, F = F1 ∧ ⋅⋅⋅ ∧ Fh, R = R1 ∧ ⋅⋅⋅ ∧ Ri, P = P1 ∧ ⋅⋅⋅ ∧ Pk.
The command above succeeds if both the following holds:
-
there is a trace of S that satisfies all the environmental assumptions and fairness conditions, and reaches a state that satisfies all the reachability conditions; that is, if the following LTL formula is satisfiable (in the chosen background theory):
IS ∧ always TS ∧ always A ∧ always eventually F ∧ eventually R
-
every property Pj is invariant for S under the environmental assumptions and the fairness conditions; that is, if the following LTL formula is valid (in the chosen background theory):
IS ∧ always TS ∧ always A ∧ always eventually F ⇒ always P
;---------
; Arbiter
;---------
(define-system NonDetArbiter
:input ( (req1 Bool) (req2 Bool) )
:output ( (gran1 Bool) (gran2 Bool) )
:local ( (s Bool) )
:init ( (not gran1) (not gran2) ) ; nothing is granted initially
:trans (
(=> (and (not req1') (not req2'))
(and (not gran1') (not gran2')))
(=> (and req1' (not req2'))
(and 'gran1 (not gran2')))
(=> (and (not req1') req2')
(and (not gran1') gran2'))
(=> (and req1' req2')
; the unconstrained value of `s` is used as non-deterministic choice
(ite s'
(and gran1' (not gran2')
(and (not gran1') gran2'))))
)
)
(verify-system NonDetArbiter
:input ( (r1 Bool) (r2 Bool) )
:output ( (g1 Bool) (g2 Bool) )
:properties (
(p1 "Every request is immediately granted" ; not invariant
(and (=> r1 g1) (=> r2 g2))
)
(p2 "In the absence of other requests, every request is immediately granted" ; invariant
(=> (distinct r1 r2)
(and (=> r1 g1) (=> r2 g2)))
)
(p3 "A request is granted only if present" ; invariant
(and (=> g1 r1) (=> g2 r2))
)
(p4 "At most one request is granted at any one time" ; invariant
(not (and g1 g2))
)
(p5 "In case of concurrent requests one of them is always granted" ; invariant
(=> (and r1 r2) (or g1 g2))
)
(p6 "If there have been no requests so far then there have been no grants" ; invariant
(=> (historically (and (not r1) (not r2)))
(historically (and (not g1) (not g2))))
)
)
)
(verify-system NonDetArbiter
:input ( (r1 Bool) (r2 Bool) )
:output ( (g1 Bool) (g2 Bool) )
:assumptions (
(a1 "There are no concurrent requests"
(not (and r1 r2))
)
)
:properties (
(p1 "Every request is immediately granted" ; invariant
(and (=> r1 g1) (=> r2 g2))
)
)
)
;---------------
; 3-bit counter
;---------------
(define-fun toBit ((b Bool)) Int (ite b 1 0))
(define-fun toInt ( (b2 Bool) (b1 Bool) (b0 Bool) ) Bool
(+ (* 4 (toBit b2)) (* 2 (toBit b1)) (toBit b0))
)
(verify-system ThreeBitCounter
:input ( (inc Bool) (start Bool) )
:output ( (o0 Bool) (o1 Bool) (o2 Bool) )
:local ( (c0 Bool) (c1 Bool) (c2 Bool) )
:properties (
(p1 "Sanity-check invariant"
(<= 0 (toInt o2 o1 o0) 7)
)
(p2 "A start signal resets the counter to 0 in the next"
(=> (before start)
(= 0 (toInt o2 o1 o0)))
)
(p2A "Alternative formulation of p2 as a transition invariant"
(=> start
(= 0 (toInt o2' o1' o0')))
)
(p3 "If no increment requests are ever sent, the counter stays at 0"
(=> (historically (not inc))
(= (toInt o2 o1 o0) 0))
)
(p4 "If there is an increment request and the counter is below 7
then it will increase by 1 next"
(let ( (n (toInt o2 o1 o0)) )
(=> (and inc (< n 7))
(= (toInt o2' o1' o0') (+ n 1))))
)
)
)
(define-system DelayedCounter
:input ( (inc Bool) (start Bool) )
:output ( (n Int) )
:local ( (c Int) )
:init (
(= n 0)
(= c (ite (and inc (not start)) 1 0))
)
:trans (
(= n' c)
(= c' (ite start' 0
(ite (not inc') c
(ite (= c 7) 0 (+ c 1)))))
)
)
(define-system CountObserver
:input ( (inc Bool) (start Bool) )
:output ( (n1 Int) (n2 Int) )
:local ( (o0 Bool) (o1 Bool) (o2 Bool) )
:init (
(= n1 (count o2 o1 o0))
(ThreeBitCounter inc start o0 o1 o2)
(DelayedCounter inc start n2)
)
:trans (
(= n1' (count o2' o1' o0'))
(ThreeBitCounter inc start o0 o1 o2)
(DelayedCounter inc start n2)
)
)
; more concisely
(define-system CountObserver
:input ( (inc Bool) (start Bool) )
:output ( (n1 Int) (n2 Int) )
:local ( (o0 Bool) (o1 Bool) (o2 Bool) )
:inv ( (= n1 (count o2 o1 o0)) )
:compose (
(ThreeBitCounter inc start o0 o1 o2)
(DelayedCounter inc start n2)
)
)
(verify-system CountObserver
:input ( (inc Bool) (start Bool) )
:output ( (n1 Int) (n2 Int) )
:properties (
(p1 "" (= n1 n2)) ; not invariant
(p2 "" (since start (= n1 n2))) ; not invariant
(p3 "" (=> (once start) (since start (= n1 n2)))) ; invariant
)
)[more]
; +-----------------------------------+
; | ThermostatController |
; | |
; | +--------------------+ |
; --up----------->| | |
; | | SetDesiredTemp |--+----------set_temp-->
; --down--------->| | | |
; | +--------------------+ | |
; | v |
; | +--------------------------+ |
; -switch-------->| |-------cool-->
; | | ControlTemp | |
; -out_temp------>| |-------heat-->
; | +--------------------------+ |
; | |
; +-----------------------------------+
;-------------------
; Global parameters
;-------------------
;
(define-const MIN_TEMP Real 40.0)
(define-const MAX_TEMP Real 100.0)
(define-const INI_TEMP Real 70.0)
(define-const DEADBAND Real 3.0)
(define-const DIFF Real 3.0)
(declare-enum-sort SwitchPos (Cool Off Heat))
;----------------
; SetDesiredTemp
;----------------
;
(define-system SetDesiredTemp
:input ( (up_button Bool) (down_button Bool) )
:output ( (set_temp Real) )
:auxiliary (
(inc Bool
:def (and up_button (<= set_temp (- MAX_TEMP DIFF))))
(dec Bool
:def (and down_button (>= set_temp (+ MIN_TEMP DIFF))))
)
:assumptions (
(a1 "Up/Down button signals are mutually exclusive"
(not (and up_button down_button))
)
)
:guarantees (
(g0 "Initial set_temp"
(initially (= set_temp INIT_TEMP))
)
(g1 "set_temp increment"
(=> inc (= set_temp' (+ set_temp DIFF)))
)
(g2 "set_temp decrement"
(=> dec (= set_temp' (- set_temp DIFF)))
)
(g3 "set_temp invariance"
(=> (not (or inc dec))
(= set_temp' set_temp))
)
)
)
;-------------
; ControlTemp
;-------------
;
(define-system ControlTemp
:input ( (switch SwitchPos) (current_temp Real) (set_temp Real) )
:output ( (cool_act_sig Bool) (heat_act_sig Bool) )
:auxiliary (
(cool_start Bool
:def (and (= switch Cool)
(> current_temp (+ set_temp DEADBAND)))
)
(cool_mode Bool
:init cool_start
:next (or cool_start'
(and cool_mode
(= switch' Cool)
(> current_temp' set_temp')))
)
(heat_start Bool
:def (and (= switch Heat)
(< current_temp (- set_temp DEADBAND)))
)
(heat_mode Bool
:init heat_start
:next (or heat_start'
(and heat_mode
(= switch' Heat)
(< current_temp' set_temp')))
)
(off_mode Bool
:def (and (not cool_mode) (not heat_mode))
)
)
:guarantees (
(g1 "Cooling activation"
(= cool_act_sig cool_mode)
)
(g2 "Heating activation"
(= heat_act_sig heat_mode)
)
(g3 "Heating and cooling mutually exclusive"
(not (and heat_act_sig cool_act_sig))
)
)
)
;----------------------
; ThermostatController
;----------------------
;
(define-system ThermostatController
:input ( (switch SwitchPo) (up Bool) (down Bool) (in_temp Real) )
:output ( (cool Bool) (heat Bool) (set_tempReal) )
:inv (
(SetDesireTemp up down set_temp)
(ControlTemp switch in_temp set_temp cool heat)
)
:assumptions (
(a1 "Up/Down button signals are mutually exclusive"
(not (and up_button down_button))
)
)
:auxiliary (
(in_deadzone Bool
:def (<= (- set_temp DEADBAND) in_temp (+ set_temp DEADBAND))
)
(system_off Bool
:def (and (not cool) (not heat))
)
)
:guarantees (
(g1 "Initial temperature is in range":
(<= MIN_TEM INIT_TEMP MAX_TEMP)
)
(g2 "Deadband and Diff are positive values"
(and (> DEADBAND 0.0) (> DIFF 0.0))
)
(g3 "No activation signal is enabled if switch is in Off"
(=> (= switch Off) (and (not cool) (not heat)))
)
(g4 "Cooling system is turned On only if switch is in Cool"
(=> cool (= switch Cool))
)
(g5 "Heating system is turned On only if switch is in Heat"
(=> cool (= switch Heat))
)
(g6 "Activation signals are never enabled at the same time"
(not (and cool heat))
)
(g7 "set_temp is always in range"
(<= MIN_TEMP set_temp MAX_TEMP)
)
(g8 "set_temp doesn't change if no button is pressed"
(=> (and (not up') (not down')
(= set_temp' set_temp))
)
(g9 "set_temp doesn't decrease if the up button is pressed"
(=> up'
(>= set_temp' set_temp))
)
(g10 "set_temp doesn't increase if the down button is pressed":
(=> down'
(<= set_temp' set_temp))
)
(g11 "System is Off if indoor temperature is in the dead zone and system was Off in the previous step"
(=> (and in_deadzone' system_off) system_off')
)
(g12 "Cooling system is On only if indoor temperature is higher than set_temp":
(=> cool (> in_temp set_temp))
)
(g13 "Heating system is On only if indoor temperature is lower than set_temp":
(=> heat (< in_temp set_temp))
)
(g14 "Cooling system is On if switch is in Cool and the indoor temperature is higher than set_temp plus deadband"
(=> (and (= switch Cool) (> in_temp (+ set_temp DEADBAND)))
cool)
)
(g15 "Heating system is On if switch is in Heat and the indoor temperature is lower than set_temp plus deadband"
(=> (and (= switch Heat) (> in_temp (+ set_temp DEADBAND)))
cool)
)
(g16 "Once cooling system is On, it remains On as long as set_temp has not been reached and switch is in Cool"
(=> (and (since cool (= switch Cool))
(> in_temp set_temp))
cool))
)
(g17 "Once heating system is On, it remains On as long as set_temp has not been reached and switch is in Heat"
(=> (and (since heat (= switch Heat))
(< in_temp set_temp))
heat))
)
)
)[parameters as rigid variables]