License, terms of use and compatibility

This software is Copyright (C) 2024 Maciej Sobczak (www.inspirel.com).

This file is distributed under the GPL 3.0 license.

This assistant is intended for evaluation and as support for education activities.
Please contact Inspirel if you need other terms of use or if you would like to deploy this assistant in a professional, commercial or industrial environment. Or for any other reason.

This notebook was entirely tested with:

$Version

It should work with comparable Wolfram installations as well.

Since the underlying (Wolfram) engine might change with each update, its capability to solve different verification problems can change, too. This means in that in future versions some examples and models presented here might be simplified.

Documentation

How to use this document

This file is a Wolfram notebook that combines source code for useful functions and definitions, documentation (this section) and a set of examples.

Only the source code needs to be here to support your own work. It is configured as initialization code, so that it will evaluate automatically before any other code is executed. As such, the easiest way to use this notebook is to write and just evaluate your own code at the bottom of this notebook. Good luck!

The documentation part and examples can be safely removed if you need to reduce the size of this file, or if you prefer to work with multiple documents (for your own projects, perhaps) but don’t need to keep the copies of documentation and examples everywhere.

The examples are relatively complete demonstrations of what can be done and can be also used as a catalogue of patterns and idioms for reuse. In a sense, the set of examples also serves as a set of regression tests for the main source code.

Many examples (especially the ones for Event-B modeling) were inspired by models described in the book "Modeling in Event-B" by Jean-Raymond Abrial and no amount of comment can replace the complete exposition in that book, but still, hopefully, the models are clear enough to be understood on their own. Note that even though the variable names and general modeling strategy correspond to book examples, some details were changed to reflect the Wolfram syntax rules and supported theories.

What it can do

The functionality of Formal Assistant is built on top of standard Wolfram functions and the general capability of the Wolfram language to perform symbolic computations and to solve both arithmetic and logic problems. The Formal Assistant is supposed to be modular and extendable and to support these goals it is designed in layers.

The most basic layer (let’s call it “Level 0”) is of course the Wolfram system itself - everything it can do, can be embedded and mixed with other things, so in this sense the expressive capability of the Assistant is unlimited. On the other hand, the basic Wolfram functions and language syntax have their own limits that influence what and how things can be expressed and solved.

The first layer of added functionality (“Level 1”) deals with the general concept of deduction. That is, given a set of symbols or values, and a set of transformation rules, the Assistant can deduce something by repeatedly applying the given rules. The deduction layer can also generate a trace of deductions and can display the results by linking them with inputs and applicable rules.

A set of “standard rules” exist to support deduction by means of reducing, simplifying and solving sets of equations, inequalities and logic statements. These standard rules can be plugged explicitly to the deduction layer, but they also form implicit foundation for higher level functions.

Further (“Level 2”), two high-level functions support validation and satisfiability checks that are key tools in formal verification. These functions have multiple options that allow to plug in customized “theorems” that are automatically combined with given questions. Basic set definitions, n-ary predicates and quantifiers with those predicates are also supported in a way that allows to efficiently resolve typical verification questions.

Finally (“Level 3”), a relatively complete modeling method (inspired by Event-B) is supported by means of function that gathers information from the given model and generates multiple verification checks to ensure correctness of the model and its subsequent refinements.

Most likely future developments of the Formal Assistant will focus on expanding the capability and expressiveness of “Level 3” - either by improving the Event-B modeling, or by supporting other modeling methods.

Base functions (Level 1)

deduceStep

deduceStep[knowns_,rules_,OptionsPattern[{finalTerms->{},knownIndexThreshold->1,verbose->Automatic}]]:=...

This function performs a single deduction step and returns a list of results, each being a triple {res,ruleNum,inputs}, where res is a new value, ruleNum is the index of rule that produced that value and inputs is a list of positions from knowns.

knowns is a list of “things” - values, symbols, expressions, etc.

rules is a list of transformation rules. Each rule (expressed with Rule[a,b] or just a->b) defines how the elements from the list of knowns (left-hand can be a list for n-ary transformations) should be selected and transformed into new value (which can be a list as well).
As a special case, right-hand can be a Function, which is evaluated to produce the new value.
All rules are applied to all relevant combinations of knowns (depending on arity of the given rule) in a single deduction step.

finalTerms is an optional list of values (or a test Function) that terminate the deduction.

knownIndexThreshold is an index in the list of knowns above which rules are applied (that is, knowns below that index are not used).

verbose can be False, Counts, True or Automatic to select various levels of verbosity.

deduce

deduce[knowns_List,rules_List,OptionsPattern[{finalTerms->{},withTrace->False,maxSteps->10,verbose->Automatic}]]:=...

This function repeatedly performs deduction steps as long as new (distinct) values are produced or until a final term is reached or maximum number of steps is executed.

knowns, rules, finalTerms and verbose are as in deduceStep.

withTrace decides if the rule and input trace (in the form as in deduceStep) is part of the output, in which case it is a second element of the pair {result,trace}.

maxSteps is a limit on the number of deduction steps.

verbose can be False, Counts, True or Automatic to select various levels of verbosity.

showSteps

showSteps[result_,rules_,OptionsPattern[{prune->True}]]:=...

This function pretty-prints the deduction trace obtained from deduce.

result is the output from deduce (if called using withTrace->True).

rules should be the same set of rules that was used with deduce.

prune clears the list of results from entries that are not on paths that reached final True or False values.

Validators (Level 2)

validate

validate[knowns_,question_,OptionsPattern[{theorems->{},maxSteps->3,verbose->Automatic}]]:=...

This function performs the test for implication knowns=>question and returns False, True or Indeterminate (if the result cannot be computed or confirmed either way using available methods).

knowns is a conjunction (And[...]) of terms or a single term.
The term can be:
- equation (like x==0, y==x+1, z==True, etc.),
- inequality (like x>0, 0≤x≤y+7, etc.),
- declaration of domain or set membership (like x∈Integers, y∈Booleans, z∈{1,2,3,4}, etc.),
- free n-ary predicate (like P[x,y], but it is expected that the same predicate is used somewhere in knowns or question within a quantifier), negation of such predicate (like ¬P[x,y]) or
- quantified expression (ForAll or Exists) over a single variable with (possibly negated) n-ary predicate as the only quantified expression (like ForAll[x,0≤x≤10,P[x]]).
Note that predicates, on their own, should be undefined symbols - it is their interaction with quantifiers and other instances of the same (or negated) predicates that allows them to be replaced with ultimate logic values. In this sense predicates are always “ghost” predicates.
For convenience, Span[a,b] is recognized as well and resolves to appropriate inequality, depending on the way it is used.
Many of the standard Wolfram functions can be also used as parts of these expressions - in principle, all the functions that can be used within FullSimplify, Reduce and FindInstance.

question is a conjunction of terms or a single term (as in knowns).

theorems is a list of "name"->theorem, where theorem is one of:
- implication of the form A=>B or (Subscript[A, 1])∧(Subscript[A, 2])∧...=>C - in this case, if A is found among top-level terms in knowns, C is automatically added to knowns as well,
- replacement of the form A->B - such rules are applied to both knowns and question with the use of standard ReplaceAll function.
- Function[{knowns,question}, ...] or separately defined function of the same profile, which can rewrite the whole set in arbitrary way.

maxSteps is a limit on the number of deduction steps.

verbose can be False, Monitor, Counts, True or Automatic to select various levels of verbosity.

validatePiecewise

validatePiecewise[knowns_,question_,OptionsPattern[{theorems->{},parallel->False,maxSteps->3,verbose->Automatic}]]:=...

This function has the same purpose and arguments as validate, but identifies variables of finite domains (Booleans and simple sets) and validates the given problem separately for each possible value assignments for all such variables. As such, it offers a trade-off:
- it replaces a single problem with multiple (possibly large number) other problems, but
- each of them can be a lot simpler to solve than the original.

This function should be treated as a backup solution if validate takes too long or fails to solve the given problem. On the other hand, the possibility to solve those smaller problems in multiple parallel kernels (if the target platform allows that) might offer performance improvements.

All arguments have the same meaning as in validate, except:

parallel attempts to launch individual validations in separate kernels.

satisfy

satisfy[problem_,OptionsPattern[{theorems->{},maxSteps->3,verbose->Automatic}]]:=...

This function checks if the given problem has at least one solution and returns False, True or Indeterminate (if the result cannot be computed or confirmed either way using available methods).

problem is a conjunction of terms, interpreted as knowns in validate.

The remaining options are treated as in validate.

Event-B modeling (Level 3)

validateModel

validateModel[m_model,OptionsPattern[{onlyPhase->"*",onlyEvents->"*",onlyInvariants->"*",method->Full,parallel->False,showProofs->False,verbose->Automatic}]]:=...

This function validates the given model by generating appropriate verification checks, evaluating them and printing results.

m is a model to be checked. The model can contain axioms, theorems, invariants, variants, initialization conditions and events with guards and actions. It can also refine one more abstract model. See the list of special symbols that can be used to define models below.

onlyPhase is a string pattern that selects the particular verification phases to be executed. Possible phase names are:
- init,
- events,
- guards,
- invariants,
- superposition,
- convergence,
- deadlock.

onlyEvents is a string pattern that selects the names of events to be verified.

onlyInvariants is a string pattern that selects the names of invariants to be verified.

method is one of:
- Full, which tries to solve every generated model check at once, or
- Piecewise, which detects Boolean variables and simple set membership declarations and tries to solve the given problem with all possible replacements of those variables with their domains’ values.
For each check generated for the model, Piecewise execution transforms a (possibly large) single problem into many simpler problems, which might help in cases where underlying methods cannot cope with original statements. Piecewise execution might be slower (because there are many invocations of underlying Wolfram functions instead of one) or faster (because after replacing some of the variables with constant values the problem can be significantly simpler to solve). When combined with parallel->True, Piecewise execution of those simplified problems in every model check is parallelized, but individual model checks are processed in sequence.

parallel indicates whether parallel execution of model checks is intended. If method is Full (see above), then model checks are parallelized across multiple invariants; if method is Piecewise, individual model checks are processed in sequence, but they are potentially parallelized across Boolean and set membership replacements.

showProofs allows to print, in tabular form, the knowns and questions for each generated model check. This option helps in debugging failing checks.

verbose can be Total, Less, False, Monitor, Counts, True or Automatic to select various levels of verbosity.

Model checks

See “Event-B verification checks” subsection in examples (below) for a demonstration of possible model checks.

Symbols with special meaning in models

The Event-B modeling layer is built on top of regular Wolfram syntax and is governed by all Wolfram grammar and operator precedence rules. Still, some symbols have special meaning that contribute to the model structure and its expressive power (the actual strategies of using these elements in modeling activities are beyond the scope of this documentation):

model is a main wrapper for the model description:

myModel=model[...];

refines can appear once at top level in the model and indicates the base (abstract) model, which is refined by the given model.

myBaseModel=model[...];
myModel=model[
refines[myBaseModel], (* myModel refines myBaseModel *)
...
];

axiom can appear at top level in the model and introduces an axiom to the set of knowns in all generated checks:

myModel=model[
axiom["axiom1",a>0], (* a>0 is present in knowns of all checks *)
...
];

invariant can appear at top level in the model and introduces an invariant that is verified and used as a known depending on the particular model check:

myModel=model[
invariant["inv1",a>0], (* a>0 is verified and used in knowns of some checks *)
...
];

variant can appear at top level in the model and introduces a variant for convergent events:

myModel=model[
variant["var1",n-a], (* n-a is verified to be non-negative and decreasing in each convergent event *)
...
];

theorem can appear at top level in the model and introduces a transformation step that is applied to knowns and questions before the attempt to solve a given problem (theorems are applied in order):

myModel=model[
theorem["th1",A\[Implies]B], (* if A is present at top-level in knowns, B will be added to knowns as well *)

theorem["th2",A->B], (* A->B replacement is applied across the whole problem *)

theorem["th3",myTheorem], (* myTheorem is a function that can arbitrarily process and transform both knowns and question for all generated checks *)

...
];

init can appear at top level in the model and introduces initial conditions for invariants:

myModel=model[
init["init1",{a->7,b->42}], (* initial values for variables a and b *)
...
];

event can appear at top level in the model:

myModel=model[
event["ev1",... (* (optional) guards and actions *)],
...
];

when is an optional guard for the event:

myModel=model[
event["ev1",
when[a>b, (* a>b is a condition for the event to be activated *)
... (* actions *)
]
],
...
];

convergent or convergent[] is an explicit declaration (or suppression, if negated) of convergence for the event (new non-refining events in refined models are convergent by default) - the given event is supposed to strictly decrease the model’s variant.
anticipated or anticipated[] is a declaration of “weak” convergence - the given event is supposed not to increase the model’s variant:

myModel=model[
variant[(* ... *)],
event["ev1",
convergent, (* this event is convergent - variant should decrease *)
... (* guards and actions *)
],
event["ev2", (* this event is anticipated - variant should not increase *)
anticipated,
... (* guards and actions *)
],
event["ev3",
¬convergent, (* this event is NOT convergent - variant is not checked *)
... (* guards and actions *)
],
...
];

Rule expresses initialization and event actions, it looks like (and in fact is, internally) a replacement rule:

myModel=model[
init["init1",a->7], (* initial value for variable a *)
event["ev1",
a->a+1 (* a is incremented by this event *)
],
...
];

Rule also allows to explicitly name a base event for refining event (be default events refine base events of the same name):

myBaseModel=model[
event["bev",...]
];
myModel=model[
refines[myBaseModel],
event["ev"->"bev", (* "ev" refines "bev" *)
...
]
];

List allows to group initialization and event actions, guard conditions and multiple base events in the event refinement declaration:

myModel=model[
refines[...],

init["init1",{a->7,b->42}], (* multiple initializations *)

event["ev"->{"ev1","ev2"}, (* multiple base events *)
when[{a>b,c>d}, (* multiple guards (same as AND) *)
{a->a+1,b->0} (* multiple actions *)
]
],
...
];

Null is equivalent to an empty list:

myModel=model[
event["ev",
when[a>b,
Null (* no action (useful to mark a terminating event in a state machine) *)
]
],
...
];

Element defines domain and simple set membership:

myModel=model[
invariant["inv1",k∈(Integers)], (* k is expected to be an Integer *)
invariant["inv2",m∈{7,42,101}], (* m is one of these values *)
...
];

Span defines a range:

myModel=model[
invariant["inv1",r∈Span[1,n]], (* equivalent to 1 ≤ r ≤ n *)
...
];

Exists and ForAll can be used with predicates:

myModel=model[
invariant["inv1",ForAll[x,x∈Span[1,r-1],¬good[x]]],
invariant["inv2",Exists[x,x∈Span[r,n],good[x]]],
...
];

deadlockFree or deadlockFree[] can appear at top level of the model and switches on checks for deadlock freedom (that disjunction of all event guards covers the whole space defined by invariants):

myModel=model[
deadlockFree[], (* myModel will be checked for deadlock freedom *)
...
];

Otherwise, everything is just plain Wolfram.

Code (do not remove)

Core Proof Assistant

(* helper, ensures the value is a list *)
ensureList[v_]:=
If[ListQ[v],
v,
If[v===Null,
{}, (* treat direct Null as empty list *)
List[v]
]
]

(* helper for pretty-printing results *)
prettyResult[res_]:=Switch[res,
True,Style[res,Bold,Green],
False,Style[res,Bold,Red],
_,Style[res,Bold,Black]
]

(* helper, checks if the term is considered final *)
isFinalTerm[t_,finalTermsOpt_]:=
If[ListQ[finalTermsOpt],
(* final terms is a list - check membership *)
MemberQ[finalTermsOpt,t],
(* otherwise treat finalTerms as a function that checks for termination *)
finalTermsOpt[t]
]

(*
Returns a list of new knowns, deduced from knowns and rules,
or an empty list if nothing new can be deduced;
knownIndexThreshold is the cut-off index in knowns, so that only rules that apply to premises from this index and above are processed (this is to avoid processing old premises over and over again in subsequent steps;

each result in the returned list has form: {term,ruleIndex,{premiseIndex1,...}}
*)
deduceStep[knowns_,rules_,OptionsPattern[{finalTerms->{},knownIndexThreshold->1,verbose->Automatic}]]:=Module[
{
newKnowns={},
ruleIndex,
candidatePositions, (* list of lists of term positions, for the given rule *)
candidatePremises, (* lists of terms from knowns that match rule premises, for each separate rule application *)
result, (* result from the application of each rule *)

finalTermsOpt=OptionValue[finalTerms],
knownIndexThresholdOpt=OptionValue[knownIndexThreshold],
verboseOpt=OptionValue[verbose],
ruleLoggedOnce,
applicationCount
},

If[verboseOpt===Automatic,
verboseOpt=False
];

If[verboseOpt===Counts,
Print["    terms: ",Length[knowns]]
];

applicationCount=0;
Catch[
(* process each rule in the list *)
ruleIndex=0;
Scan[
Function[rule, (* rule is {premise,...}\[Implies]conclusion *)

++ruleIndex;
If[verboseOpt,
ruleLoggedOnce=False
];

With[
{
premises=rule[[1]],
conclusion=rule[[2]]
},

(* for each premise in the rule,collect positions of terms from knowns that can be used for that premise *)
(* candidatePositions is the list of lists:
{{pos1ForPremise1,pos2ForPremise1...},{pos1ForPremise2,...}},...} *)
candidatePositions={};
Scan[
Function[prem, (* each premise from the current rule *)
AppendTo[candidatePositions,Position[knowns,prem,{1},Heads->False]]
],
premises
];

(* apply index threshold to avoid processing rules on old knowns repeatedly;
that is, if the candidates are all from below the threashold, it means that they were already processed in previous deduction steps and there is no need to repeat that processing (because it would give the same results that were already added to knowns) *)
If[Max[Flatten[candidatePositions]]>knownIndexThresholdOpt,

(* apply rule to each combination of candidates found above *)
Scan[
Function[candidates, (* positions for each set of candidates *)

(* again, prune selections that were already processed (those below the index threshold);in addition, if the candidates positions have duplicates, it means that the same premise was selected more than once for the given rule (this can happen with patterns in rules) - omit this selection, process only selections of unique premises *)
If[Max[Flatten[candidates]]>knownIndexThresholdOpt&&DuplicateFreeQ[candidates],

candidatePremises=Extract[knowns,#]&/@candidates;

(* re-check the candidate premises by treating them as a whole, against the premises treated as a single list-based pattern *)
If[MatchQ[candidatePremises,premises],

If[verboseOpt,
If[Not[ruleLoggedOnce],
Print["processing rule ",ruleIndex,": ",rule];
ruleLoggedOnce=True
];
Print["        on: ",StringJoin@Riffle[ToString/@candidatePremises,", "]]
];

If[Head[conclusion]===Function,
(* functional rule - supply candidate premises and produce new term *)
result=conclusion@@candidatePremises,

(* literal rule - the rule provides the result and is not parameterized by premises *)
result=conclusion
];

result=ensureList[result];

++applicationCount;

If[verboseOpt,
Print["     gives: ",StringJoin@Riffle[ToString/@result,", "]]
],

(* the candidate premises do not match the whole sequence of premises (that is, treated together as a single pattern), even though they were found and collected by matching each premise pattern separately *)
result={}
];

Scan[
Function[res,
If[isFinalTerm[res,finalTermsOpt],
(* this step produced conclusive final term - no need to continue processing, but ensure this is still added to the known list, even if it would repeat the existing known (for example, it might happen that True or False was in the knowns from the beginning, but we still need proper deduction trace for deduce[] to recognize that there will be no more steps to execute *)
AppendTo[newKnowns,{res,ruleIndex,Flatten[candidates]}];
Throw[Null]
];

If[Not[MemberQ[knowns,res]],
AppendTo[newKnowns,{res,ruleIndex,Flatten[candidates]}]
]
],
result
]
]
],
(* assume that all rules are orderless: *)
Union[Sort/@Tuples[candidatePositions]]

(* if ordering of premises is important this is more appropriate instead of the above, optimized version: *)
(*Tuples[candidatePositions]*)
]
]
]
],
rules
]
];

If[verboseOpt===Counts,
Print["    rule applications: ",applicationCount]
];

DeleteDuplicatesBy[newKnowns,First]
]

deduce[knowns_List,rules_List,OptionsPattern[{finalTerms->{},withTrace->False,maxSteps->10,verbose->Automatic}]]:=Module[
{
trace,
oldKnownsLength=0,
currentKnowns=knowns,
stepResult,
newKnowns,newTrace,
finalTermsOpt=OptionValue[finalTerms],
withTraceOpt=OptionValue[withTrace],
maxStepsOpt=OptionValue[maxSteps],
stepCount=0,
keepWork=True,
verboseOpt=OptionValue[verbose]
},

If[verboseOpt===Automatic,
verboseOpt=False
];

trace=Table[{0,{}},Length[knowns]];

While[keepWork,
++stepCount;

If[verboseOpt===Counts||verboseOpt===True,
Print["step ",stepCount]
];

stepResult=deduceStep[currentKnowns,rules,finalTerms->finalTermsOpt,knownIndexThreshold->oldKnownsLength,verbose->verboseOpt];

If[stepResult==={},
If[verboseOpt,
Print["Cannot deduce more terms or final term reached."]
];
keepWork=False,

newKnowns=stepResult[[All,1]];
newTrace=stepResult[[All,2;;]];

oldKnownsLength=Length[currentKnowns];
currentKnowns=Join[currentKnowns,newKnowns];
trace=Join[trace,newTrace];

With[
{
lastKnown=Last[newKnowns]
},
If[isFinalTerm[lastKnown,finalTermsOpt],
keepWork=False
]
]
];

If[stepCount==maxStepsOpt,
If[verboseOpt,
Print["Max number of steps reached, aborting."]
];
keepWork=False
]
];

If[withTraceOpt,
{currentKnowns,trace},
currentKnowns
]
]

(* gives a short summary of the result, as True, False or Indeterminate *)
finalResult[result_]:=With[
{
last=result[[-1]]
},

Switch[last,
True|False,last,
_,Indeterminate
]
]

(* prints the list of deductions, from the beginning;
if the deduction finishes with True or False, the list is pruned to show only those deductions that trace to that final result *)

(* helper for recursive back-tracing, collects indices of those terms that are reachable from the end *)
collectReachableIndices[zipped_,index_]:=With[
{
entry=zipped[[index]]
},

Join[{index},Catenate[collectReachableIndices[zipped,#]&/@entry[[3]]]]
]

showSteps[result_,rules_,OptionsPattern[{prune->True}]]:=Module[
{
terms=result[[1]],
trace=result[[2]],
resultLen,
zipped,
pruneOpt=OptionValue[prune],
pruned={},
prunedIndices,
prunedLen
},

zipped=Transpose[{terms,trace[[All,1]],trace[[All,2]]}];

resultLen=Length[zipped];

(* prune the list if the deduction finishes with True or False *)
If[pruneOpt&&(Last[terms]===True||Last[terms]===False),

(* prepend recursively those deductions that are reachable from the end *)
prunedIndices=Union[collectReachableIndices[zipped,resultLen]];
pruned=zipped[[prunedIndices]],

(* otherwise, do not prune and show the whole list *)
pruned=zipped
];

prunedLen=Length[pruned];

If[prunedLen==resultLen,
Print["Showing all entries."],
Print["Skipping ",resultLen-prunedLen," irrelevant entries."]
];

Scan[
Function[d, (* d is {term,ruleIndex,{premiseIndex1,...}} *)
With[
{
term=d[[1]],
ruleIndex=d[[2]], (* rule index points to the rule that is a source for the given term and is 0 for any of the terms in initial set (knowns) *)
rule=rules[[d[[2]]]],
premises=terms[[d[[3]]]]
},

(* show only deductions for terms that did not exist in knowns) *)
If[ruleIndex≠0,
Print[StandardForm[rule]];
Print["    with: ",StringJoin@Riffle[ToString/@premises,", "]];
Print["   gives: ",term]
]
]
],
pruned
]
]

(* simple wrapper for use with standard rules *)
showSteps[result_]:=showSteps[result,standardRules];

(* helper for handling Span variables expressions, extracts Span "declarations" of the form a ∈ Span and prepares list of replacements, so that span variables can be replaced with expanded forms Span[aMin,aMax];
returns both the list of replacements and the term with declarations removed *)
extractSpanDeclarations[term_]:=Module[
{
spanVariables,
spanVarReplacements,
result
},

(* gather and remove direct span variable declarations, they are "declared" as a ∈ Span *)
spanVariables=Cases[term,Element[v_Symbol,Span]:>v,{0,Infinity}];
result=DeleteCases[term,Element[_Symbol,Span]];

(* replace all span variables with span expressions like Span[xMin,xMax] *)spanVarReplacements=Map[
Function[v,
With[
{
vStr=ToString[v]
},
v->Span[Unique[vStr<>"Min"],Unique[vStr<>"Max"]]
]
],
spanVariables
];

{spanVarReplacements,result}
]

(* helper, replaces expressions of the form a ∈ SomeSet, where SomeSet can be:
- Span (for span declarations),
- {a,b,c,...} for explicit set definitions,
- Booleans;
Set memberships like a∈Integers and a∈Reals are preserved, because they are hints for further computations.
Set membership a∈Booleans can be preserved with leaveBooleans->True option.
*)
rewriteSets[term_,spanVarReplacements_,OptionsPattern[{leaveBooleans->False}]]:=Module[
{
leaveBooleansOpt=OptionValue[leaveBooleans],
result
},

(* replace span variables, according to earlier declarations *)
result=term/.spanVarReplacements;

If[leaveBooleansOpt==False,
(* expand a ∈ Booleans *)
result=result/.Element[name_Symbol,Booleans]:>(name==False||name==True)
];

(* expand a ∈ {...} *)
result=result/.Element[el_,set_List]:>Or@@(el==#&/@set);

(* type preservation for Span operations *)
(* ∅ ∈ Span *)
result=result/.Element[∅,Span]->True;
(* Span[a,b] ∈ Span *)
result=result/.Element[Span[_,_],Span]->True;
(* Span[a,b]+Span[b,c] ∈ Span *)
result=result/.Element[Span[a_,b_]+Span[c_,d_],Span]:>(b+1==c||d+1==a);
(* Span[a,b]+c ∈ Span *)
result=result/.Element[Plus[Span[a_,b_],c_],Span]:>(c+1==a||b+1==c);

(* arithmetic and equalities *)
(* Span[a,b]==∅ *)
result=result/.Equal[Span[a_,b_],∅]:>(a>b);
(* Span[a,b]==Span[c,d] *)
result=result/.Equal[Span[a_,b_],Span[c_,d_]]:>(a==c&&b==d);
(* Span[a,b]+c == Span[d,e] *)
result=result/.Equal[Span[a_,b_]+c_,Span[d_,e_]]:>((a==d&&b+1==c&&c==e)||(c+1==a&&c==d&&b==e));
(* Span[a,b]+Span[c,d] == Span[e,f] *)
(* TODO: uncomment if needed *)
(*result=result/.Equal[Span[a_,b_]+Span[c_,d_],Span[e_,f_]]:>((a==e&&b+1==c&&d==f)||(c==e&&d+1==a&&b==f));*)

(* handle x ∈ Span[a,b], inject x ∈ Integers if x is a symbol *)
result=result/.Element[expr_,Span[a_,b_]]:>
If[Head[expr]===Symbol,
Element[expr,Integers]&&(a≤expr≤b),
(a≤expr≤b)
];
(* handle x ∉ Span[a,b] *)
result=result/.NotElement[expr_,Span[a_,b_]]:>Not[(a≤expr≤b)];
(*result=result/.Element[v_Integer,Span[a_,b_]]:>(a≤v≤b);*)
(*result=result/.Element[el_Symbol,Span[a_,b_]]:>(a≤el≤b);*)

(* handle a ∈ ∅ *)
(* TODO: uncomment if needed *)
(*result = result/.Element[_,∅]->False;*)

result
]

(* helpers, used to structurally match n-ary predicates *)
regionMatchPrerequisite[uv_Symbol,quantSet1_,quantSet2_,failingResult_]:=Module[
{
region1=quantSet1[[1]],
params1=quantSet1[[2]],
region2=quantSet2[[1]],
params2=quantSet2[[2]],
lastUVMatch={}
},

If[Length[params1]==Length[params2],
And@@MapThread[
Function[{p1,p2}, (* p1,p2 are respective parameters *)

If[p1===uv&&p2===uv,
(* both params refer to bound variable uv *)
If[lastUVMatch=={},
(* first-time match with uv *)
lastUVMatch={p1,p2} ;
True,

lastUVMatch==={p1,p2}
],

If[p1===uv&&p2=!=uv,
(* left param refers to uv, fail this match *)
failingResult,

If[p1=!=uv&&p2===uv,
(* right param refers to uv, add condition *)

If[lastUVMatch=={},
(* first-time match with uv *)
lastUVMatch={p1,p2} ;
p1==uv,

lastUVMatch==={p1,p2}
],

p1===p2 (* require exact structural match for free parameters *)
]
]
]
],
{params1,params2}
],

failingResult
]
]
regionMatchCondition[uv_Symbol,quantSet1_,quantSet2_,failingResult_]:=Module[
{
region1=quantSet1[[1]],
params1=quantSet1[[2]],
region2=quantSet2[[1]],
params2=quantSet2[[2]],
lastUVMatch={},
match
},

match=regionMatchPrerequisite[uv,quantSet1,quantSet2,failingResult];

If[match===True,
region1\[Implies]region2,
If[match===failingResult,
match,
match\[Implies]region2
]
]
]

(* helper, replaces expressions of the forms:
- ForAll[var,varSet,P[var]], where varSet is some constraining condition on var and P is a symbol denoting some arbitrary unary predicate,
- P[var]
These expressions do not need to use the same var, which is replaced with unified and unique name anyway; expressions are matched by the predicate name;
predicates can be used directly or negated.
These expressions are deleted from knowns and in question replaced with conditions that make them True if appropriate set dependencies are met.
*)
rewriteQuantifiers[knowns_,question_]:=Module[
{
knowns2, (* after preprocessing *)
knownsFAPos, (* positions of ForAll expressions *)
knownsEXPos, (* positions of Exists expressions *)
knownsPredPos={}, (* positions of free predicates in knowns *)
questionFAPos,
questionEXPos,
combinedKnownsFASets=<||>, (* combined FA variable sets, keyed by predicate head *)
combinedKnownsFANSets=<||>, (* combined variable sets for negated predicates *)
combinedKnownsEXSets=<||>, (* combined EX variable sets, keyed by predicate head *)
combinedKnownsEXNSets=<||>, (* combined variable sets for negated predicates *)
unifiedVars=<||>, (* unified variable names for FA and EX regions *)
kfa,kfaVar,kfaCond,kfaPred,kfaPredHead,
kex,kexVar,kexCond,kexPred,kexPredHead,
quantSet, (* condition set for the given quantifier *)
kPredPos,kPred,
uv, (* unique variable name to replace bound variable *)
merged,newQS,keepTrying, (* temporary object for merging sets *)
qfa,qfaVar,qfaCond,qfaPred,qfaPredHead,qPreds,qPr,
qex,qexVar,qexCond,qexPred,qexPredHead,
cond,ncond,qRep,
questionReplacements={}, (* transformations in question *)
injectedKnowns (* new knowns deduced from quantifier sets *)
},

(* 0. perform some obvious transformations, like:
ForAll[P&&Q] -> ForAll[P] && ForAll[Q]
*)
knowns2=Replace[knowns,
fa_ForAll:>With[
{
var=fa[[1]],
cnd=fa[[2]],
pred=fa[[3]]
},
If[Head[pred]===And,
Map[
Function[p,
ForAll[var,cnd,p]
],
pred
],
fa
]
],
{0,1}
];

If[MatchQ[knowns2,ForAll[_,_,_]],
knownsFAPos={{}},
knownsFAPos=Position[knowns2,ForAll[_,_,_],{1}]
];
If[MatchQ[knowns2,Exists[_,_,_]],
knownsEXPos={{}},
knownsEXPos=Position[knowns2,Exists[_,_,_],{1}]
];
If[MatchQ[question,ForAll[_,_,_]],
questionFAPos={{}},
questionFAPos=Position[question,ForAll[_,_,_],{1}]
];
If[MatchQ[question,Exists[_,_,_]],
questionEXPos={{}},
questionEXPos=Position[question,Exists[_,_,_],{1}]
];

(* 1. find and merge FA, EX and free predicates from knowns *)

(* 1a. find all FA quantifiers and store their ranges and parameters with the use of unified variables *)
(* Note: for P and !P predicates variables are the same, but their sets are collected separately *)
Scan[
Function[kpos, (* kpos is position of FA quantifier in knowns *)
kfa=If[kpos=={},knowns2,Extract[knowns2,kpos]];
kfaVar=kfa[[1]]; (* variable *)
kfaCond=kfa[[2]]; (* constraining condition *)
kfaPred=kfa[[3]]; (* predicate *)

If[Head[kfaVar]===Symbol&&
Max@@Length/@Position[kfaPred,kfaVar]==1, (* n-ary predicates over one variable are supported *)

kfaPredHead=Head[kfaPred]; (* predicate name *)

If[KeyExistsQ[unifiedVars,kfaPredHead],
uv=unifiedVars[kfaPredHead],

uv=Unique[ToString[kfaPredHead]];
unifiedVars[kfaPredHead]=uv
];

quantSet={
(kfaCond/.kfaVar->uv), (* region of the quantifier *)
(List@@kfaPred/.kfaVar->uv) (* predicate parameters *)
};

If[KeyExistsQ[combinedKnownsFASets,kfaPredHead],
(* note: sets are kept separate, in a list *)
AppendTo[combinedKnownsFASets[kfaPredHead],quantSet],
combinedKnownsFASets[kfaPredHead]={quantSet}
],

If[Head[kfaPred]===Not&&
Head[kfaVar]===Symbol&&
Max@@Length/@Position[kfaPred[[1]],kfaVar]==1,
(* negation of predicate, accumulate separate set for that name *)

kfaPredHead=Head[kfaPred[[1]]]; (* predicate name *)

If[KeyExistsQ[unifiedVars,kfaPredHead],
uv=unifiedVars[kfaPredHead],

uv=Unique[ToString[kfaPredHead]];
unifiedVars[kfaPredHead]=uv
];

quantSet={
(kfaCond/.kfaVar->uv), (* region of the quantifier *)
(List@@kfaPred[[1]]/.kfaVar->uv) (* predicate parameters *)
};

If[KeyExistsQ[combinedKnownsFANSets,kfaPredHead],
(* note: sets are kept separate, in a list *)
AppendTo[combinedKnownsFANSets[kfaPredHead],quantSet],
combinedKnownsFANSets[kfaPredHead]={quantSet}
],

Print["quantifier ",kfa," is not supported (wrong predicate)"];
Abort[]
]
]
],
knownsFAPos
];

(* 1b. find all EX quantifiers and store their ranges and parameters with the use of unified variables *)
(* Note: the EX sets cannot be merged the way FA sets are, they need to preserve their separate meaning and impact on further deductions;
that's why combinedKnownsEXSets keeps lists of separate sets instead of merging them into a single set *)
Scan[
Function[kpos, (* kpos is position of EX quantifier in knowns *)
kex=If[kpos=={},knowns2,Extract[knowns2,kpos]];
kexVar=kex[[1]]; (* variable *)
kexCond=kex[[2]]; (* constraining condition *)
kexPred=kex[[3]]; (* predicate *)

If[Head[kexVar]===Symbol&&
Max@@Length/@Position[kexPred,kexVar]==1, (* n-ary predicates over one variable are supported *)

kexPredHead=Head[kexPred]; (* predicate name *)

If[KeyExistsQ[unifiedVars,kexPredHead],
uv=unifiedVars[kexPredHead],

uv=Unique[ToString[kexPredHead]];
unifiedVars[kexPredHead]=uv
];

quantSet={
(kexCond/.kexVar->uv), (* region of the quantifier *)
(List@@kexPred/.kexVar->uv) (* predicate parameters *)
};

If[KeyExistsQ[combinedKnownsEXSets,kexPredHead],
(* note: sets are kept separate, in a list *)
AppendTo[combinedKnownsEXSets[kexPredHead],quantSet],
combinedKnownsEXSets[kexPredHead]={quantSet}
],

If[Head[kexPred]===Not&&
Head[kexVar]===Symbol&&
Max@@Length/@Position[kexPred[[1]],kexVar]==1,
(* negation of predicate, accumulate separate set for that name *)

kexPredHead=Head[kexPred[[1]]]; (* predicate name *)

If[KeyExistsQ[unifiedVars,kexPredHead],
uv=unifiedVars[kexPredHead],

uv=Unique[ToString[kexPredHead]];
unifiedVars[kexPredHead]=uv
];

quantSet={
(kexCond/.kexVar->uv), (* region of the quantifier *)
(List@@kexPred[[1]]/.kexVar->uv) (* predicate parameters *)
};

If[KeyExistsQ[combinedKnownsEXNSets,kexPredHead],
(* note: sets are kept separate, in a list *)
AppendTo[combinedKnownsEXNSets[kexPredHead],quantSet],
combinedKnownsEXNSets[kexPredHead]={quantSet}
],

Print["quantifier ",kex," is not supported (wrong predicate)"];
Abort[]
]
]
],
knownsEXPos
];

(* 1c. find FA and EX quantifiers in question as well and collect their predicate names, so that they can be recognized in knowns even if they exist there in free form only *)
Scan[
Function[qpos, (* qpos is position of FA or EX quantifier in question *)
qfa=If[qpos=={},question,Extract[question,qpos]];
qfaVar=qfa[[1]]; (* variable *)
qfaPred=qfa[[3]]; (* predicate *)

If[Head[qfaVar]===Symbol&&
Max@@Length/@Position[qfaPred,qfaVar]==1,  (* n-ary predicates over one variable are supported *)

qfaPredHead=Head[qfaPred]; (* predicate name *)

If[Not[KeyExistsQ[unifiedVars,qfaPredHead]],
uv=Unique[ToString[qfaPredHead]];
unifiedVars[qfaPredHead]=uv
],

If[Head[qfaPred]===Not&&
Head[qfaVar]===Symbol&&
Max@@Length/@Position[qfaPred[[1]],qfaVar]==1,  
(* negation of predicate, accumulate separate set for that name *)

qfaPredHead=Head[qfaPred[[1]]]; (* predicate name *)

If[Not[KeyExistsQ[unifiedVars,qfaPredHead]],
uv=Unique[ToString[qfaPredHead]];
unifiedVars[qfaPredHead]=uv
],

Print["quantifier ",qfa," is not supported (wrong predicate)"];
Abort[]
]
]
],
Union[questionFAPos,questionEXPos]
];

(* 1d. find all free predicates in knowns or their negations (those that were used in quantifiers) and add them to combinedKnownsFASets *)
Scan[
Function[ph, (* ph is predicate head, one of those found in quantifiers *)

uv=unifiedVars[ph];

(* find predicates used directly (without negation) *)
If[MatchQ[knowns2,_ForAll|_Exists],
kPredPos={}, (* ignore predicate if ForAll or Exists is the whole knowns *)
kPredPos=Position[knowns2,_ph,{1}]
];

Scan[
Function[kpos, (* kpos is position of free predicate in knowns *)
kPred=If[kpos=={},knowns2,Extract[knowns2,kpos]];

AppendTo[knownsPredPos,kpos];

If[Length[kPred]==1,
quantSet={
uv==kPred[[1]], (* implicit region for unary predicate *)
{uv} (* implicit parameter for unary predicate *)
},
quantSet={
True, (* implicit region for n-ary predicate *)
List@@kPred (* parameters *)
}
];

If[KeyExistsQ[combinedKnownsFASets,ph],
AppendTo[combinedKnownsFASets[ph],quantSet],
combinedKnownsFASets[ph]={quantSet}
];
(*
If[KeyExistsQ[combinedKnownsEXSets,ph],
AppendTo[combinedKnownsEXSets[ph],quantSet],
combinedKnownsEXSets[ph]={quantSet}
]
*)
],
kPredPos
];

(* find negated predicates as well *)
If[MatchQ[knowns2,_ForAll|_Exists],
kPredPos={}, (* ignore predicate if ForAll or Exists is the whole knowns *)
kPredPos=Position[knowns2,Not[_ph],{1}]
];

Scan[
Function[kpos, (* kpos is position of free negated predicate in knowns *)
kPred=If[kpos=={},knowns2,Extract[knowns2,kpos]][[1]];

AppendTo[knownsPredPos,kpos];

If[Length[kPred]==1,
quantSet={
uv==kPred[[1]], (* implicit region for unary predicate *)
{uv} (* implicit parameter for unary predicate *)
},
quantSet={
True, (* implicit region for n-ary predicate *)
List@@kPred (* parameters *)
}
];

If[KeyExistsQ[combinedKnownsFANSets,ph],
AppendTo[combinedKnownsFANSets[ph],quantSet],
combinedKnownsFANSets[ph]={quantSet}
];
(*
If[KeyExistsQ[combinedKnownsEXNSets,ph],
AppendTo[combinedKnownsEXNSets[ph],quantSet],
combinedKnownsEXNSets[ph]={quantSet}
]
*)
],
kPredPos
]
],
Keys[unifiedVars]
];

(* 1e. merge regions of FA and FAN quantifiers *)

keepTrying=True;
While[keepTrying,
keepTrying=False;
merged=<||>;
Scan[
Function[ph, (* ph is predicate name that has some FA sets *)

merged[ph]={};
uv=unifiedVars[ph];

Scan[
Function[qss, (* qss are two of FA {region,params} sets from knowns *)
With[
{
region1=qss[[1,1]],
params1=qss[[1,2]],
region2=qss[[2,1]],
params2=qss[[2,2]]
},

newQS=None;
If[params1===params2&&FreeQ[region1,region2]&&FreeQ[region2,region1],
newQS={Or@@Union[List@@(region1||region2)],params1},

cond=regionMatchPrerequisite[uv,qss[[1]],qss[[2]],False];
If[cond=!=False&&cond=!=True&&FreeQ[region2,cond],
newQS={cond||region2,params2},

cond=regionMatchPrerequisite[uv,qss[[2]],qss[[1]],False];
If[cond=!=False&&cond=!=True&&FreeQ[region1,cond],
newQS={region1||cond,params1}
]
]
];

If[newQS=!=None&&FreeQ[combinedKnownsFASets[ph],newQS],
keepTrying=True;
AppendTo[merged[ph],newQS]
]
]
],
Subsets[combinedKnownsFASets[ph],{2}]
]
],
Keys[combinedKnownsFASets]
];
Scan[
Function[ph,
combinedKnownsFASets[ph]=Union[Join[combinedKnownsFASets[ph],merged[ph]]]
],
Keys[merged]
]
];

(* and FAN sets as well: *)
keepTrying=True;
While[keepTrying,
keepTrying=False;
merged=<||>;
Scan[
Function[ph, (* ph is predicate name that has some FAN sets *)

merged[ph]={};
uv=unifiedVars[ph];

Scan[
Function[qss, (* qss are two of FAN {region,params} sets from knowns *)
With[
{
region1=qss[[1,1]],
params1=qss[[1,2]],
region2=qss[[2,1]],
params2=qss[[2,2]]
},

newQS=None;
If[params1===params2&&FreeQ[region1,region2]&&FreeQ[region2,region1],
newQS={Or@@Union[List@@(region1||region2)],params1},

cond=regionMatchPrerequisite[uv,qss[[1]],qss[[2]],False];
If[cond=!=False&&cond=!=True&&FreeQ[region2,cond],
newQS={cond||region2,params2},

cond=regionMatchPrerequisite[uv,qss[[2]],qss[[1]],False];
If[cond=!=False&&cond=!=True&&FreeQ[region1,cond],
newQS={region1||cond,params1}
]
]
];

If[newQS=!=None&&FreeQ[combinedKnownsFANSets[ph],newQS],
keepTrying=True;
AppendTo[merged[ph],newQS]
]
]
],
Subsets[combinedKnownsFANSets[ph],{2}]
]
],
Keys[combinedKnownsFANSets]
];
Scan[
Function[ph,
combinedKnownsFANSets[ph]=Union[Join[combinedKnownsFANSets[ph],merged[ph]]]
],
Keys[merged]
]
];

(* 2. find quantifiers and free predicates in question and prepare replacement rules for them *)

(* 2a. find FA quantifiers *)
Scan[
Function[qpos, (* qpos is position of FA quantifier in question *)
qfa=If[qpos=={},question,Extract[question,qpos]];
qfaVar=qfa[[1]]; (* variable *)
qfaCond=qfa[[2]]; (* constraining condition *)
qfaPred=qfa[[3]];

If[Head[qfaVar]===Symbol&&
Max@@Length/@Position[qfaPred,qfaVar]==1, (* quantifier with direct (non-negated) predicate *)

qfaPredHead=Head[qfaPred];

uv=unifiedVars[qfaPredHead];

quantSet={
(qfaCond/.qfaVar->uv), (* region *)
(List@@qfaPred/.qfaVar->uv) (* parameters *)
};

If[KeyExistsQ[combinedKnownsFASets,qfaPredHead],
qRep=False;
Scan[
Function[qs, (* qs is one of FA {region,parameters} from knowns *)
qRep=qRep||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFASets[qfaPredHead]
],

(* no such predicate was used in knowns, so this FA in question resolves against empty known set, irrespective of its parameters *)
qRep=quantSet[[1]]\[Implies]False
];

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep],

If[MatchQ[qfaPred,Not[_]]&&MemberQ[qfaPred[[1]],qfaVar],
(* quantifier with negated predicate *)

qfaPredHead=Head[qfaPred[[1]]];

uv=unifiedVars[qfaPredHead];

quantSet={
(qfaCond/.qfaVar->uv), (* region *)
(List@@qfaPred[[1]]/.qfaVar->uv) (* parameters *)
};

If[KeyExistsQ[combinedKnownsFANSets,qfaPredHead],
qRep=False;
Scan[
Function[qs, (* qs is one of FAN {region,parameters} from knowns *)
qRep=qRep||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFANSets[qfaPredHead]
],

(* no such predicate was used in knowns, so this FAN in question resolves against empty known set, irrespective of its parameters *)
qRep=quantSet[[1]]\[Implies]False
];

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep],

Print["quantifier ",qfa," is not supported (wrong predicate)"];
Abort[]
]
]
],
questionFAPos
];

(* 2b. find EX quantifiers *)
Scan[
Function[qpos, (* qpos is position of EX quantifier in question *)
qex=If[qpos=={},question,Extract[question,qpos]];
qexVar=qex[[1]]; (* variable *)
qexCond=qex[[2]]; (* constraining condition *)
qexPred=qex[[3]];

If[Head[qexVar]===Symbol&&
Max@@Length/@Position[qexPred,qfaVar]==1,
(* quantifier with direct (non-negated) predicate *)

qexPredHead=Head[qexPred];

uv=unifiedVars[qexPredHead];

quantSet={
(qexCond/.qexVar->uv), (* region *)
(List@@qexPred/.qexVar->uv) (* parameters *)
};

qRep=False;
If[KeyExistsQ[combinedKnownsEXSets,qexPredHead],
Scan[
Function[qs, (* qs is one of EX {region,parameters} from knowns *)
qRep=qRep||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXSets[qexPredHead]
],

(* no such predicate was used in knowns, so this EX in question resolves against empty known set, irrespective of its parameters *)
qRep=quantSet[[1]]\[Implies]False
];
If[KeyExistsQ[combinedKnownsFANSets,qexPredHead],
Scan[
Function[qs, (* qs is one of FAN {region,parameters} from knowns *)
qRep=qRep&&!regionMatchCondition[uv,quantSet,qs,Indeterminate]
],
combinedKnownsFANSets[qexPredHead]
]
];
If[KeyExistsQ[combinedKnownsFASets,qexPredHead],
Scan[
Function[qs, (* qs is one of FA {region,parameters} from knowns *)
qRep=qRep||satisfy[regionMatchCondition[uv,quantSet,qs,Indeterminate]]
],
combinedKnownsFASets[qexPredHead]
]
];

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep],

If[MatchQ[qexPred,Not[_]]&&MemberQ[qexPred[[1]],qexVar],
(* quantifier with negated predicate *)

qexPredHead=Head[qexPred[[1]]];

uv=unifiedVars[qexPredHead];

quantSet={
(qexCond/.qexVar->uv), (* region *)
(List@@qexPred[[1]]/.qexVar->uv) (* parameters *)
};

qRep=False;
If[KeyExistsQ[combinedKnownsEXNSets,qexPredHead],
Scan[
Function[qs, (* qs is one of EXN {region,parameters} from knowns *)
qRep=qRep||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXNSets[qexPredHead]
],

(* no such predicate was used in knowns, so this EXN in question resolves against empty known set, irrespective of its parameters *)
qRep=quantSet[[1]]\[Implies]False
];
If[KeyExistsQ[combinedKnownsFASets,qexPredHead],
Scan[
Function[qs, (* qs is one of FAN {region,parameters} from knowns *)
qRep=qRep&&!regionMatchCondition[uv,quantSet,qs,Indeterminate]
],
combinedKnownsFASets[qexPredHead]
]
];
If[KeyExistsQ[combinedKnownsFANSets,qexPredHead],
Scan[
Function[qs, (* qs is one of FA {region,parameters} from knowns *)
qRep=qRep||satisfy[regionMatchCondition[uv,quantSet,qs,Indeterminate]]
],
combinedKnownsFANSets[qexPredHead]
]
];

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep],

Print["quantifier ",qex," is not supported (wrong predicate)"];
Abort[]
]
]
],
questionEXPos
];

(* 2c. find also free uses of predicates in question *)
(* direct (non-negated) predicates: *)
Scan[
Function[ph, (* ph is predicate name *)
If[MatchQ[question,_ph],
qPreds={{}}, (* whole question is ph[...] *)
If[MatchQ[question,Not[_ph]],
qPreds={}, (* whole question is Not[ph[...]] - ignore *)
If[MatchQ[question,_ForAll|_Exists],
qPreds={}, (* whole question is ForAll or Exists - ignore *)
qPreds=Position[question,_ph,{1}]
]
]
];

uv=unifiedVars[ph];

Scan[
Function[qpos, (* qpos is position of free predicate in question *)
qPr=If[qpos=={},question,Extract[question,qpos]];

quantSet={
True, (* implicit region for free predicate *)
List@@qPr (* parameters *)
};

cond=False;
If[KeyExistsQ[combinedKnownsFASets,ph],
Scan[
Function[qs, (* qs is one of FA {region,params} from knowns *)
cond=cond||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFASets[ph]
]
];
If[KeyExistsQ[combinedKnownsEXSets,ph],
Scan[
Function[qs, (* qs is one of EX {region,params} from knowns *)
cond=cond||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXSets[ph]
]
];

(* additionally, match based on value equality with free predicates in knowns *)
(* free predicates in knowns were added to both FA and EX sets with True regions (and with no reference to univied var), so it is enough to match only one of them (let's say FA) *)
If[KeyExistsQ[combinedKnownsFASets,ph],
Scan[
Function[qs, (* qs is one of FA {region,params} from knowns *)
With[
{
region=qs[[1]],
params=qs[[2]],
qP=quantSet[[2]] (* parameters of the processed predicate *)
},
If[region===True&&FreeQ[params,uv],
cond=cond||And@@Thread[qP==params]
]
]
],
combinedKnownsFASets[ph]
]
];

ncond=False;
If[KeyExistsQ[combinedKnownsFANSets,ph],
Scan[
Function[qs, (* qs is one of FAN {region,params} from knowns *)
ncond=ncond||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFANSets[ph]
]
];
If[KeyExistsQ[combinedKnownsEXNSets,ph],
Scan[
Function[qs, (* qs is one of EXN {region,params} from knowns *)
ncond=ncond||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXNSets[ph]
]
];

(* additionally, match based on value equality with free predicates in knowns *)
If[KeyExistsQ[combinedKnownsFANSets,ph],
Scan[
Function[qs, (* qs is one of FAN {region,params} from knowns *)
With[
{
region=qs[[1]],
params=qs[[2]],
qP=quantSet[[2]] (* parameters of the processed predicate *)
},
If[region===True&&FreeQ[params,uv],
ncond=ncond||And@@Thread[qP==params]
]
]
],
combinedKnownsFANSets[ph]
]
];

qRep=cond&&!ncond;

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep]
],
qPreds
]
],
Keys[unifiedVars]
];

(* 2c, negated predicates: *)
Scan[
Function[ph, (* ph is predicate name *)
If[MatchQ[question,Not[_ph]],
qPreds={{}},
If[MatchQ[question,_ForAll|_Exists],
qPreds={}, (* ignore *)
qPreds=Position[question,Not[_ph],{1}]
]
];

uv=unifiedVars[ph];

Scan[
Function[qpos, (* qpos is position of free predicate in question *)
qPr=If[qpos=={},question,Extract[question,qpos]][[1]];

quantSet={
True, (* implicit region for free predicate *)
List@@qPr (* parameters *)
};

cond=False;
If[KeyExistsQ[combinedKnownsFANSets,ph],
Scan[
Function[qs, (* qs is one of FAN {region,params} from knowns *)
cond=cond||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFANSets[ph]
]];
If[KeyExistsQ[combinedKnownsEXNSets,ph],
Scan[
Function[qs, (* qs is one of EXN {region,params} from knowns *)
cond=cond||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXNSets[ph]
]
];

(* additionally, match based on value equality with free predicates in knowns *)
(* free predicates in knowns were added to both FA and EX sets with True regions (and with no reference to univied var), so it is enough to match only one of them (let's say FA) *)
If[KeyExistsQ[combinedKnownsFANSets,ph],
Scan[
Function[qs, (* qs is one of FAN {region,params} from knowns *)
With[
{
region=qs[[1]],
params=qs[[2]],
qP=quantSet[[2]] (* parameters of the processed predicate *)
},
If[region===True&&FreeQ[params,uv],
cond=cond||And@@Thread[qP==params]
]
]
],
combinedKnownsFANSets[ph]
]
];

ncond=False;
If[KeyExistsQ[combinedKnownsFASets,ph],
Scan[
Function[qs, (* qs is one of FA {region,params} from knowns *)
ncond=ncond||regionMatchCondition[uv,quantSet,qs,False]
],
combinedKnownsFASets[ph]
]
];
If[KeyExistsQ[combinedKnownsEXSets,ph],
Scan[
Function[qs, (* qs is one of EX {region,params} from knowns *)
ncond=ncond||regionMatchCondition[uv,qs,quantSet,False]
],
combinedKnownsEXSets[ph]
]
];

(* additionally, match based on value equality with free predicates in knowns *)
If[KeyExistsQ[combinedKnownsFASets,ph],
Scan[
Function[qs, (* qs is one of FA {region,params} from knowns *)
With[
{
region=qs[[1]],
params=qs[[2]],
qP=quantSet[[2]] (* parameters of the processed predicate *)
},
If[region===True&&FreeQ[params,uv],
ncond=ncond||And@@Thread[qP==params]
]
]
],
combinedKnownsFASets[ph]
]
];

qRep=cond&&!ncond;

AppendTo[questionReplacements,If[qpos=={},{{}},qpos]->qRep]
],
qPreds
]
],
Keys[unifiedVars]
];

(* 3. deduce injected knowns *)

(* 3a. collect knowns from EX and EXN sets (pruned by FAN and FA sets, respectively) as they can be interpreted as "assertions" that something, somewhere is true *)

injectedKnowns=True;
Scan[
Function[ph, (* ph is predicate name in any of combined EX set *)
Scan[
Function[ex, (* ex is one of EX {region,params} for the given predicate name *)
injectedKnowns=injectedKnowns&&ex[[1]]
],
combinedKnownsEXSets[ph]
];
If[KeyExistsQ[combinedKnownsFANSets,ph],
Scan[
Function[fan, (* fan is one of FAN {region,params} for the given predicate name *)
injectedKnowns=injectedKnowns&&!fan[[1]]
],
combinedKnownsFANSets[ph]
]
]
],
Keys[combinedKnownsEXSets]
];
Scan[
Function[ph, (* ph is predicate name in any of combined EXN set *)
Scan[
Function[exn, (* exn is one of EXN {region,params} for the given predicate name *)
injectedKnowns=injectedKnowns&&exn[[1]]
],
combinedKnownsEXNSets[ph]
];
If[KeyExistsQ[combinedKnownsFASets,ph],
Scan[
Function[fa, (* fa is one of FA {region,params} for the given predicate name *)
injectedKnowns=injectedKnowns&&!fa[[1]]
],
combinedKnownsFASets[ph]
]
]
],
Keys[combinedKnownsEXNSets]
];

(*
Print["after 2c"];
Print["EX sets: ",combinedKnownsEXSets];
Print["EXN sets: ",combinedKnownsEXNSets];
Print["FA sets: ",combinedKnownsFASets];
Print["FAN sets: ",combinedKnownsFANSets];
Print["combinedVars: ",unifiedVars];
Print["questionReplacements: ",questionReplacements];
Print["injectedKnowns: ",injectedKnowns];
*)

With[
{
posToDelete=Union[knownsFAPos,knownsEXPos,knownsPredPos]
},

{
(* rewritten knowns *)
If[posToDelete=={{}},
injectedKnowns,
Delete[knowns2,posToDelete]&&injectedKnowns
],

(* rewritten question *)
ReplacePart[question,questionReplacements]
}
]
]

(* helper, flips the result, if determinate *)
flipResult[res_]:=
Switch[res,
True,False,
False,True,
_,res
]

(* helper, applies theorem to knowns and question,
th is "name"->Function[...] or "name"->Implies[a,b] or "name"->Rule[a,b] *)
applyTheorem[knowns_,question_,th_]:=
If[Head[th[[2]]]===Implies,
(* use the implication a\[Implies]b to add b, if a is present in knowns *)
With[
{
a=th[[2,1]],
b=th[[2,2]]
},

If[Head[a]===And,
(* find all elements separately, they are not matched properly by Cases *)
If[Map[MemberQ[knowns,#]&,a],
{And[knowns,b],question},
{knowns,question}
],

If[Cases[knowns,a,{1}]≠{},
{And[knowns,b],question},
{knowns,question}
]
]
],

If[Head[th[[2]]]===Rule,
(* use the rule a->b to replace a with b in both knowns and question *)
{knowns,question}/.th[[2]],

(* otherwise, treat the theorem as executable function that rewrites both knowns and question *)
th[[2]][knowns,question]
]
]
applyTheorems[knowns_,question_,ths_List]:=Module[
{
knowns2=knowns,
question2=question
},
Scan[
Function[th, (* th is "name"->Function or "name"->Implies or "name"->Rule *)
{knowns2,question2}=applyTheorem[knowns2,question2,th]
],
ths
];
{knowns2,question2}
]

(* helper, replaces instances of !x with x==False expressions,
this helps internal solver engines *)
rewriteNots[expr_]:=expr/.Not[e_]->(e==False)

(* validation driver, facilitates use with single term as first argument;
this driver also handles x∈set entries other than x∈Reals and x∈Integers *)
validate[knowns_,question_,OptionsPattern[{theorems->{},maxSteps->3,verbose->Automatic}]]:=Module[
{
theoremsOpt=OptionValue[theorems],
maxStepsOpt=OptionValue[maxSteps],
verboseOpt=OptionValue[verbose],
knowns2,question2, (* knowns and question after application of theorems *)
spanVarReplacements,
prunedKnowns,
simpleQuestion,
res
},

(* sanity check, higher-level code uses lists to group terms, the knowns and question should come here already combined with And, Or, etc., not as raw list: *)
If[ListQ[knowns]||ListQ[question],
Print["Error: argument is a list: ",question];
Abort[]
];

If[verboseOpt=!=Skip,

(* apply optional theorems, in order *)
{knowns2,question2}=applyTheorems[knowns,question,theoremsOpt];

(* handle Spans and sets *)
{spanVarReplacements,prunedKnowns}=extractSpanDeclarations[knowns2];

prunedKnowns=rewriteSets[prunedKnowns,spanVarReplacements];

(* attempt to simplify the question *)
simpleQuestion=FullSimplify[rewriteSets[question2,spanVarReplacements]];

(* handle ForAll quantifiers and their matching free predicates *)
{prunedKnowns,simpleQuestion}=rewriteQuantifiers[prunedKnowns,simpleQuestion];

(* rewrite !x into x==False, to help internal solvers *)prunedKnowns=rewriteNots[prunedKnowns];

If[verboseOpt===Monitor,
Print["validate: ",knowns,",\n",question]
];
If[verboseOpt===True,
Print["validate: ",knowns,",\n",question];
If[theoremsOpt≠{},
Print["after theorems: ",knowns2,",\n",question2];
];
Print["validate rewritten: ",prunedKnowns,",\n",simpleQuestion]
];

res=finalResult[
deduce[
List[And[prunedKnowns,Not[simpleQuestion]]],
standardRules,finalTerms->{False},
maxSteps->maxStepsOpt,verbose->verboseOpt
]
],

res=Indeterminate
];

res=flipResult[res];

res
]

(* driver for piecewise computation of larger proofs that contain x∈{...} entries;
this driver also handles x∈set entries other than x∈Reals and x∈Integers *)
validatePiecewise[knowns_,question_,OptionsPattern[{theorems->{},parallel->False,maxSteps->3,verbose->Automatic}]]:=Module[
{
theoremsOpt=OptionValue[theorems],
maxStepsOpt=OptionValue[maxSteps],
parallelOpt=OptionValue[parallel],
verboseOpt=OptionValue[verbose],
knowns2,question2, (* knowns and question after application of theorems *)
spanVarReplacements,
parallelWrapper,
sets,
prunedKnowns,
valueAssignments,
assignmentLength,
counter, (* only for sequential progress tracking *)
simpleQuestion,
totalRes
},

(* sanity checks *)
If[ListQ[question],
Print["Error: question is a list: ",question];
Abort[]
];

If[verboseOpt=!=Skip,

If[parallelOpt,
(* process using parallel kernels *)
parallelWrapper=Parallelize,

(* process sequentially *)
parallelWrapper=Identity
];

(* apply optional theorems, in order *)
{knowns2,question2}=applyTheorems[knowns,question,theoremsOpt];

(* handle Spans and sets *)
{spanVarReplacements,prunedKnowns}=extractSpanDeclarations[knowns2];

(* attempt to simplify the question *)
simpleQuestion=FullSimplify[rewriteSets[question2,spanVarReplacements]];

(* prunedKnowns does not have to contain the entries that are gathered anyway at level 1 in sets and valueAssignments below *)
prunedKnowns=DeleteCases[prunedKnowns,Element[_Symbol,_List],1];
prunedKnowns=DeleteCases[prunedKnowns,Element[_Symbol,Booleans],1];
prunedKnowns=rewriteSets[prunedKnowns,spanVarReplacements];

(* handle ForAll quantifiers and their matching free predicates *)
{prunedKnowns,simpleQuestion}=rewriteQuantifiers[prunedKnowns,simpleQuestion];

If[verboseOpt===Monitor,
Print["validate: ",knowns,",\n",question]
];
If[verboseOpt===True,
Print["validate: ",knowns,",\n",question];
If[theoremsOpt≠{},
Print["after theorems: ",knowns2,",\n",question2];
];
Print["validate rewritten: ",prunedKnowns,",\n",simpleQuestion]
];

sets=Join[
Cases[knowns2,Element[name_Symbol,s_List],1],
Cases[knowns2,Element[name_Symbol,Booleans]:>Element[name,{True,False}],1]
];
valueAssignments=Thread[sets[[All,1]]->#]&/@Tuples[sets[[All,2]]];
assignmentLength=Length[valueAssignments];

If[parallelOpt===False,
counter=0;
PrintTemporary[
ProgressIndicator[Dynamic[counter],{0,assignmentLength}],
"  ",Dynamic[counter],"/",assignmentLength]
];

totalRes=And@@parallelWrapper[
Map[
Function[assignment,
Module[
{
res
},

res=finalResult[
deduce[
List[And[prunedKnowns,Not[simpleQuestion]]/.assignment],
standardRules,finalTerms->{False},
maxSteps->maxStepsOpt,verbose->verboseOpt
]
];

res=flipResult[res];

If[parallelOpt===False,
++counter
];

If[MemberQ[{Monitor,True},verboseOpt],
If[res=!=True,
Print[prettyResult[res]," with ",assignment]
]
];

res
]
],
valueAssignments
]
],

totalRes=Indeterminate
];

If[Head[totalRes]===And,
(* the result contains at least one Indeterminate and cannot be And-ed *)
totalRes=Indeterminate
];

totalRes
]

(* satisfiability driver, facilitates use with single term as its argument;
this driver also handles x∈set entries other than x∈Reals and x∈Integers. *)
satisfy[problem_,OptionsPattern[{theorems->{},maxSteps->3,verbose->Automatic}]]:=Module[
{
theoremsOpt=OptionValue[theorems],
maxStepsOpt=OptionValue[maxSteps],
verboseOpt=OptionValue[verbose],
problem2,dummyQuestion2, (* problem after application of theorems *)
dummyQuestion3, (* question placeholder for rewriting quantifiers *)
spanVarReplacements,
prunedProblem,
res
},

(* sanity check, higher-level code uses lists to group terms, the problem should come here already combined with And, Or, etc., not as raw list: *)
If[ListQ[problem],
Print["Error: argument is a list: ",problem];
Abort[]
];

If[verboseOpt=!=Skip,

(* apply optional theorems, in order *)
{problem2,dummyQuestion2}=applyTheorems[problem,True,theoremsOpt];

(* handle Spans and sets *)
{spanVarReplacements,prunedProblem}=extractSpanDeclarations[problem2];

prunedProblem=rewriteSets[prunedProblem,spanVarReplacements,leaveBooleans->True];

(* handle ForAll quantifiers and their matching free predicates *)
{prunedProblem,dummyQuestion3}=rewriteQuantifiers[prunedProblem,True];

If[verboseOpt===Monitor,
Print["satisfy: ",problem]
];
If[verboseOpt===True,
Print["satisfy: ",problem];
If[theoremsOpt≠{},
Print["after theorems: ",problem2];
];
Print["satisfy rewritten: ",prunedProblem]
];

res=finalResult[
deduce[
List[prunedProblem],
standardInstanceRules,finalTerms->{True,False,Indeterminate},
maxSteps->maxStepsOpt,verbose->verboseOpt
]
],

res=Indeterminate
];

res
]

(* TODO: satisfyPiecewise? *)

Standard rules

(* sometimes Reduce and FullSimplify produce different results (or only one of them can solve the problem); try both *)
trySolve[t_]:=Module[
{
vars,
r,
fs
},

vars=Complement[Union@Cases[t,_Symbol,-1],{Integers,Reals,True,False}];
(* try to resolve for each variable in turn, until conclusive result is reached *)
If[vars!={},
Catch[
Scan[
Function[v, (* v is one of vars used in t *)
r=FullSimplify@Quiet[Reduce[t,v]];
If[r===True||r===False,
Throw[r]
]
],
vars
]
],
r=t
];

If[r===True||r===False,
(* conclusive result, no need to try FullSimplify separately *)
r,

fs=FullSimplify[t];
If[r===fs,
r, (* if results are the same, use only one of them *)
If[Head[r]=!=Reduce,
{r,fs}, (* results are different *)
fs (* Reduce failed and remained unevaluated *)
]
]
]
]

(* standard deduction rules for formula simplification *)
standardRules={
(* attempt to reduce and simplify the terms individually *)
{_}->({x}|->trySolve[x]),

(* attempt to combine terms *)
{x_,y_}->({x,y}|->trySolve[And[x,y]])
};

(* returns (possibly empty) list of instances or Indeterminate *)
tryFindInstance[t_]:=Module[
{
fs,
vars,
instances
},

vars=Complement[Union@Cases[t,_Symbol,-1],{Booleans,Integers,Reals,True,False}];

If[vars≠{},
instances=Quiet@FindInstance[t,vars],
instances=If[trySolve[t]==True,{True},{}]
];

If[ListQ[instances],
Length[instances]>0,
Indeterminate
]
]

(* standard deduction rules for finding solution instances *)
standardInstanceRules={
{_}->({x}|->tryFindInstance[x])
};

Event-B modeling

Current limitations:
- More abstract set operations and functions expressed as set products are not supported.
- Event parameters are not supported.
- Witness predicates are not supported.

(* Event-B style of modeling *)

(* helpers for displaying proofs *)
prettyProof[caption_String,knowns_List,question_List]:=Print[
Grid[
{
{caption,SpanFromLeft},
{Column@knowns,Column@question}
},
Alignment->Left,Frame->All,Spacings->{1,1}
]
]
prettyReachabilityProof[caption_String,knowns_List]:=Print[
Grid[
{
{caption},
{Column@knowns}
},
Alignment->Left,Frame->All,Spacings->{1,1}
]
]
prettyPath[names_List]:=StringJoin[Riffle[names," -> "]]

(* helpers for decomposing event names "ownName"->"refinedName" *)
properName[fullName_]:=If[StringQ[fullName],fullName,fullName[[1]]]
separateNames[fullName_]:=
If[StringQ[fullName],
{fullName,{fullName}},

(* note: fullName[[2]] can be a list of strings, if the event is merging,
so the list is always returned for unification *)
{fullName[[1]],ensureList[fullName[[2]]]}
]

(* helper for dividing actions (including init actions) into deterministic assignments and non-deterministic promises *)
splitActionsPromises[acts_]:=Module[
{
groups,
actions,
promises
},

groups=GroupBy[acts,Head[#]===Rule&];
actions=Lookup[groups,True,{}]; (* actions or empty list *)
promises=Lookup[groups,False,{}]; (* promises or empty list *)

{actions,promises}
]

(* helper for extracting guards (if present) and actions (and promises) from events *)
guardsAndActions[e_event]:=Module[
{
pruned=DeleteCases[e,
_convergent|convergent|Not[_convergent]|Not[convergent]|
_anticipated|anticipated,
1],
guards,
actions,
promises
},

If[Head[pruned[[2]]]===when,
(* the event has guards and actions, in when[guards,actions] *)
guards=ensureList[pruned[[2,1]]];
{actions,promises}=splitActionsPromises[ensureList[pruned[[2,2]]]],

(* there is no guard, only actions *)
guards={};
{actions,promises}=splitActionsPromises[ensureList[pruned[[2]]]]
];

{guards,actions,promises}
]

(* helper, collects all guards (ORed at first level and ANDed at second) from the list of events, used for deadlock freedom check *)
allGuards[events_List]:=If[events≠{},
Or@@Map[
Function[ev,
Module[
{
guards,
dummyActions,
dummyPromises
},
{guards,dummyActions,dummyPromises}=guardsAndActions[ev];
And@@guards
]
],
events
],
True
]

(* convergent / anticipated / not convergent events:
- convergent: the variant is checked to be limited and lowering when action takes place (if this is selected, the variant is not checked for anticipation);
- anticipated: the variant is checked to be limited and not growing when action takes place (if this is selected, the variant is not checked for convergence);
- not convergent: the variant is not checked at all for this event,
this setting overrides all other flags and implicit defaults *)

(* helper for detecting convergence and non-convergence option of the event;
the default flag is True for new events in refining models, otherwise False *)
isConvergent[e_event,default_]:=If[default,
FreeQ[e,_anticipated|anticipated|Not[_convergent]|Not[convergent],1],
MemberQ[e,_convergent|convergent,1]
]

(* helper for detecting whether event is anticipated;
convergence flags are stronger than anticipated flag, so if there is any explicit setting related to convergence, the anticipation flag is not taken into account,
and the hypothetical "Not[anticipated]" setting is covered by Not[convergent] anyway *)
isAnticipated[e_event]:=MemberQ[e,_anticipated|anticipated,1]&&
FreeQ[e,_convergent|convergent|Not[_convergent]|Not[convergent],1]

(* helper, leaf events are those events that can be further refined (that is, they were not yet hidden by their own refinements) *)
leafEvents[m_model]:=Module[
{
base,
baseLeafs,
theseEvents, (* events from this model only (no base) *)
thisName,baseName,
explicitlyRefinedNames, (* names mentioned explicitly like in "env2"->"env1" *)
missedNames,
baseNamesThatAreRefined, (* names that are to be hidden by these events *)
stillVisibleBaseEvents
},

theseEvents=Cases[m,_event];

base=Cases[m,b_refines:>b[[1]]];
If[base≠{},
(* there is a base model *)
base=First[base]; (* Cases returns a list, even if single-element *)
baseLeafs=leafEvents[base];

explicitlyRefinedNames=Flatten@Map[
Function[ev, (* ev is event[...] *)
If[Head[ev[[1]]]===Rule,
ensureList[ev[[1,2]]],
Nothing
]
],
theseEvents
];
missedNames=Complement[explicitlyRefinedNames,properName/@baseLeafs[[All,1]]];
If[missedNames≠{},
Print["These names were not found in base model: ",StringJoin@Riffle[missedNames,", "]];
Abort[]
];

baseNamesThatAreRefined=Flatten@Map[
Function[ev, (* ev is event[...] *)
{thisName,baseName}=separateNames[ev[[1]]];
baseName
],
theseEvents
];
stillVisibleBaseEvents=Select[baseLeafs,FreeQ[baseNamesThatAreRefined,properName[#[[1]]]]&];
Join[theseEvents,stillVisibleBaseEvents],

(* m is the most base model, all its events are leafs *)
theseEvents
]
]

(* helper, turns the argument into a Rule (provided it has proper structure) *)
toRule[t_]:=If[Length[t]==2&&StringQ[t[[1]]],
Rule@@t,
Print["The entity should have two parts and first should be a name: ",t];
Abort[]
]

(* helper, collects guards and actions on a path that leads from the given named event in the model down via the refinement relation, returning potentially multiple paths if there are merging events on the way;
input is a currently collected single path {names,guards,actions,promises},
returns list of paths, each path is a quadruple {names,guards,actions,promises} *)
collectGuardPaths[currentPath_,
m_model,eventName_String,appendGuard_]:=Module[
{
base,
thisEvent, (* event from m, named by eventName *)
thisGuards,thisActions,thisPromises,
name,refinedNames,
furtherPath, (* currentPath extended by further elements *)
mergedResults
},

thisEvent=Select[leafEvents[m],eventName==properName[#[[1]]]&];
If[thisEvent=={},
(* event not found, return the input values without change, on one path *)
{currentPath},

(* collect actions and guards from this event and its bases (if any) *)
thisEvent=First[thisEvent];

{thisGuards,thisActions,thisPromises}=guardsAndActions[thisEvent];

(* append these values to the current path *)
If[appendGuard,
furtherPath={
DeleteDuplicates@Append[currentPath[[1]],eventName],
DeleteDuplicates@Join[currentPath[[2]],thisGuards],
DeleteDuplicates@Join[currentPath[[3]],thisActions],
DeleteDuplicates@Join[currentPath[[4]],thisPromises]
},
furtherPath={
DeleteDuplicates@Append[currentPath[[1]],eventName],
currentPath[[2]],
DeleteDuplicates@Join[currentPath[[3]],thisActions],
DeleteDuplicates@Join[currentPath[[4]],thisPromises]
}
];

base=Cases[m,b_refines:>b[[1]]];
If[base=!={},
base=First[base];

(* this is a refining model, descend *)
{name,refinedNames}=separateNames[thisEvent[[1]]];

If[Length[refinedNames]==1,
(* this event refines only one (or none) event from base model, the result is an extension of a single path;
do not collect the guard from this single base, as it is a superset of the current guard anyway *)

mergedResults=collectGuardPaths[furtherPath,base,First[refinedNames],False],

(* this event is a merging event *)
(* each merged base event creates a separate path in the refinement graph,
so the existing furtherPath list needs to be cloned, once for each refining path, with guard specific for each merged event;
collect guards from each (direct) merged event, because they are likely subsets of the current guard *)
mergedResults=Flatten[
Map[
Function[rn, (* rn is a name of each merged base event *)
collectGuardPaths[furtherPath,base,rn,True]
],
refinedNames
],
1
]
],

(* this model has no base, return single-path result *)
mergedResults={furtherPath}
];

mergedResults
]
]

(* helper for managing parallel and piecewise executions *)
doValidate[knowns_,question_,theoremsOpt_,methodOpt_,parallelOpt_,verboseOpt_]:=
If[methodOpt===Piecewise,
validatePiecewise[knowns,question,theorems->theoremsOpt,
parallel->parallelOpt,verbose->verboseOpt],
validate[knowns,question,theorems->theoremsOpt,verbose->verboseOpt]
]

(* helper, decide whether to print the result *)
showResult[res_,verboseOpt_]:=
If[res===True,
(* show success only above verbose->Less *)
verboseOpt=!=Total&&verboseOpt=!=Less,

(* show failures above verbose->Total *)
verboseOpt=!=Total
]

(* validates the complete model *)
validateModel[m_model,OptionsPattern[{onlyPhase->"*",onlyEvents->"*",onlyInvariants->"*",method->Full,parallel->False,showProofs->False,verbose->Automatic}]]:=Module[
{
base, (* base model, if m is a refinement *)
theoremsOpt,
baseTheoremsOpt,
axioms,
baseAxioms={},
inits,
baseInits={},
invariants,
baseInvariants={},
variants,
variantExprs,
axiomExprs, (* expressions from all axioms *)
baseAxiomExprs={},
invariantExprs, (* expressions from all invariants *)
baseInvariantExprs={},
thisModelEvents, (* events from this model *)
events, (* all leaf events *)
baseEvents={}, (* leaf events of the base model *)

onlyPhaseOpt=OptionValue[onlyPhase],
onlyEventsOpt=OptionValue[onlyEvents],
onlyInvariantsOpt=OptionValue[onlyInvariants],
methodOpt=OptionValue[method],
parallelOpt=OptionValue[parallel],
parallelWrapper,
showProofsOpt=OptionValue[showProofs],
verboseOpt=OptionValue[verbose],

partialResults,
results={},
counts
},

If[parallelOpt===True&&methodOpt=!=Piecewise,
parallelWrapper=Parallelize, (* parallelize some Scan calls *)
parallelWrapper=Identity (* do not parallelize *)
];

base=Cases[m,b_refines:>b[[1]]];

theoremsOpt=Cases[m,th_theorem:>toRule[th]];
axioms=Cases[m,ax_axiom:>toRule[ax]];
inits=Cases[m,i_init:>toRule[i]];
invariants=Cases[m,inv_invariant:>toRule[inv]];
variants=Cases[m,v_variant:>toRule[v]];

thisModelEvents=Cases[m,e_event];
events=leafEvents[m];

axiomExprs=Flatten[axioms[[All,2]]];
invariantExprs=Flatten[invariants[[All,2]]];
variantExprs=Flatten[variants[[All,2]]];

If[base=!={},

(* this model is a refinement of some base model, check if the refinement is correct *)

If[Length[base]=!=1,
Print["Only one base for refinement is supported."];
Abort[]
];
base=First[base]; (* simplify *)
If[Head[base]=!=model,
Print["Base model is not a proper model."];
Abort[]
];

If[verboseOpt=!=Total,
Print["This is a refining model."]
];

(* collect theorems from all bases and inject them into this model *)
baseTheoremsOpt=Cases[base,th_theorem:>toRule[th],Infinity];
theoremsOpt=Join[baseTheoremsOpt,theoremsOpt];

(* collect axioms, inits and invariants from all bases (deep) *)
baseAxioms=Cases[base,ax_axiom:>Rule@@ax,Infinity];
baseInits=Cases[base,i_init:>Rule@@i,Infinity];
baseInvariants=Cases[base,inv_invariant:>Rule@@inv,Infinity];

baseEvents=leafEvents[base];

baseAxiomExprs=Flatten[baseAxioms[[All,2]]];
baseInvariantExprs=Flatten[baseInvariants[[All,2]]],

If[verboseOpt=!=Total,
Print["This is a base model."]
];

base=Null (* simplify *)
];

(* check if all names are unique (except event names in base model) *)
With[
{
allNames=Join[
baseAxioms[[All,1]],
baseInits[[All,1]],
baseInvariants[[All,1]],
theoremsOpt[[All,1]],
axioms[[All,1]],
inits[[All,1]],
invariants[[All,1]],
variants[[All,1]],
properName/@events[[All,1]]
]
},

Scan[
Function[n,
If[Not[StringQ[n]],
Print["Improper entity name: ",n];
Abort[]
]
],
allNames
];
If[Not[DuplicateFreeQ[allNames]],
Print["These names are not unique: ",StringJoin@Riffle[Commonest[allNames],", "]];
Abort[]
]
];

(* validate all axioms and inits against invariants *)

If[StringMatchQ["init",onlyPhaseOpt],

If[verboseOpt=!=Total,
Print["Validating initial conditions."]
];

Module[
{
baseInitActions,baseInitPromises,
initActions,initPromises,
combinedInitRules (* only actions *)
},

{baseInitActions,baseInitPromises}=splitActionsPromises[Flatten[baseInits[[All,2]]]];
{initActions,initPromises}=splitActionsPromises[Flatten[inits[[All,2]]]];

combinedInitRules=Join[baseInitActions,initActions];

Module[
{
initKnowns,
baseInitQuestion,
res1,res2,res
},

initKnowns=Join[
baseAxiomExprs,axiomExprs,
baseInitActions/.Rule->Equal,
baseInitPromises,
initActions/.Rule->Equal,
initPromises
];
baseInitQuestion=Join[baseInitActions/.Rule->Equal,baseInitPromises];

If[showProofsOpt,
prettyProof["Init consistency",
initKnowns,baseInitQuestion]
];

res1=satisfy[
And@@initKnowns,
theorems->theoremsOpt,
verbose->verboseOpt
];

res2=doValidate[
And@@initKnowns,
And@@baseInitQuestion,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

res=If[res1=!=True,res1,res2];

If[showResult[res,verboseOpt],
Print["    init consistency: ",prettyResult[res]]
];

AppendTo[results,res]
];

(* check each concrete invariant *)

partialResults=parallelWrapper@Map[
Function[inv,  (* inv is name->expression *)
Module[
{
invName=inv[[1]],
invExpr=ensureList[inv[[2]]],
invExprModified=ensureList[inv[[2]]]/.combinedInitRules,
knowns,
res
},

If[StringMatchQ[invName,onlyInvariantsOpt],

knowns=Join[baseAxiomExprs,axiomExprs,
baseInitPromises,initPromises];

If[showProofsOpt,
prettyProof["Init for invariant "<>invName,
knowns,Join[invExpr,{"\nwith\n"},combinedInitRules]]
];

res=doValidate[
And@@knowns,
And@@invExprModified,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    ",invName,": ",prettyResult[res]]
];

res,

Nothing
]
]
],
invariants
];

If[partialResults≠{},
results=Join[results,partialResults],

If[showResult[Indeterminate,verboseOpt],
Print["    No invariants to check."]
]
]
]
];

(* for each event, validate strengthening of its guards and preservation of invariants of its actions *)

If[StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["guards",onlyPhaseOpt]||
StringMatchQ["invariants",onlyPhaseOpt]||
StringMatchQ["superposition",onlyPhaseOpt]||
StringMatchQ["convergence",onlyPhaseOpt],

Scan[
Function[ev, (* ev is event[...] from events (leafs of this model) *)
Module[
{
fullName=ev[[1]],
name,
refinedNames,
guards,
actions,
promises,
thisModelEventNames=properName/@thisModelEvents[[All,1]],
directlyRefinedEvents={},
baseGuards={},
basePromises={},
(*refinedEventsDeep,*) (* recursively across model hierarchy *)
(*baseActionsDeep={},*) (* recursively across model hierarchy *)
guardsActionPaths, (* collected guards and actions on all refinement paths *)
variantsAreNatural, (* for both convergent and anticipated events *)
variantsAreMonotonic, (* for convergent events *)
variantsAreNonGrowing, (* for anticipated events *)
knowns,
res
},

{name,refinedNames}=separateNames[fullName];

If[StringMatchQ[name,onlyEventsOpt],

If[verboseOpt=!=Total,
Print["Validating event ",name]
];

{guards,actions,promises}=guardsAndActions[ev];

knowns=Join[
baseAxiomExprs,axiomExprs,
baseInvariantExprs,invariantExprs,
guards
];

(* find base events that are refined by ev, only for events that exist in this model *)
If[MemberQ[thisModelEventNames,name],
directlyRefinedEvents=Select[baseEvents,
Function[bev,MemberQ[refinedNames,properName[bev[[1]]]]]
]
];

(* collect base guards, only for directly refined base events *)
If[directlyRefinedEvents≠{},
{baseGuards,basePromises}=Transpose@Map[
Function[bev, (* bev is event[...] from refinedEvents *)
Module[
{
bevGuards,
dummyBevActions,
bevPromises
},

{bevGuards,dummyBevActions,bevPromises}=guardsAndActions[bev];

{bevGuards,bevPromises}
]
],
directlyRefinedEvents
]
];

(* collect all guards and actions for this event and its bases, across the whole hierarchy *)
guardsActionPaths=collectGuardPaths[{{},{},{},{}},m,name,False];

If[StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["guards",onlyPhaseOpt],

If[guards≠{},

(* check guard reachability *)

If[showProofsOpt,
prettyReachabilityProof[
"Guard reachability for event "<>name,knowns]
];

res=satisfy[
And@@knowns,
theorems->theoremsOpt,
verbose->verboseOpt
];

If[showResult[res,verboseOpt],
Print["    guard reachable: ",prettyResult[res]]
];

AppendTo[results,res]
];

If[directlyRefinedEvents≠{},

If[verboseOpt=!=Total,
If[Length[directlyRefinedEvents]>1,
Print["    This is a merging event."],
Print["    This is a refining event."]
]
];

(* check guard and promise strengthening *)

If[Flatten[baseGuards]≠{}||(promises≠{}&&basePromises≠{}),

Module[
{
allKnowns, (* combined these guards and promises *)
allQuestions (* combined base guards and base promises *)
},

If[promises≠{},
(* there are promises in this event, check them against base ones *)
allKnowns=Join[knowns,promises];
allQuestions=Join@@@Transpose[{baseGuards,basePromises}],

(* there are no promises, do not involve base promises either *)
allKnowns=knowns;
allQuestions=baseGuards
];

If[showProofsOpt,
prettyProof["Guard and promise strengthening for event "<>name,
allKnowns,Riffle[And@@@allQuestions,"OR"]]
];

res=doValidate[
And@@allKnowns,
Or@@(And@@@allQuestions),
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
]
];

If[showResult[res,verboseOpt],
Print["    guard and promise strengthening: ",prettyResult[res]]
];

AppendTo[results,res]
] 
]
];

(* check invariant compatibility *)

If[StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["invariants",onlyPhaseOpt],

partialResults=parallelWrapper@Map[
Function[inv, (* inv is name->expression *)
Module[
{
invName=inv[[1]],
invExpr=ensureList[inv[[2]]],
invExprModified,
invRes
},

If[StringMatchQ[invName,onlyInvariantsOpt],

(* there are possibly multiple refinement paths *)
invRes=Map[
Function[path, (* path is {{names...},{guards...},{actions...}} *)
Module[
{
eventNames=path[[1]],
inheritedGuards=path[[2]],
combinedActions=DeleteDuplicatesBy[path[[3]],First],
pathKnowns,
pathRes
},

pathKnowns=Join[knowns,inheritedGuards,promises];

(* for combined actions only the first (sooner on the refinement path) modification of the given variable is taken into account to avoid replacement problems later on;
even if there are multiple modifications on a given path, they are verified by state superposition check anyway *)
combinedActions=DeleteDuplicatesBy[path[[3]],First];

invExprModified=invExpr/.combinedActions;

If[showProofsOpt,
prettyProof[
If[Length[guardsActionPaths]==1,
(* title for single refinement path *)
"Invariant compatibility for event "<>name<>" and "<>invName,
(* title for multiple refinement paths *)
"Invariant compatibility via "<>prettyPath[eventNames]<>" and "<>invName
],
pathKnowns,Join[invExpr,{"\nwith\n"},combinedActions]]
];

pathRes=doValidate[
And@@pathKnowns,
And@@invExprModified,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[pathRes,verboseOpt],
If[Length[guardsActionPaths]==1,
(* report for single refinement path *)
Print["    ",invName,": ",prettyResult[pathRes]],
(* report for multiple refinement paths *)
Print["    ",invName," via ",prettyPath[eventNames],": ",prettyResult[pathRes]]
]
];

pathRes
]
],
guardsActionPaths
];

(* invRes can be a single truth value or a list here *)
invRes,

Nothing
]
]
],
(* refined events, with their combined actions, have to be checked against both base and concrete invariants,
otherwise it would be possible for the refined action to break some base invariant that was respected by the given event in base model *)
Join[baseInvariants,invariants]
];

results=Join[results,Flatten[partialResults]]
];

(* check superposition of states, if the event is refining *)

If[(StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["superposition",onlyPhaseOpt])&&
directlyRefinedEvents≠{}, (* only if there are base events *)

(* Note: on any refinement path collected by collectGuardPaths[], duplicates are already removed - this means that only syntactically different actions have their keys (left of rule assignment) listed multiple times, so it is enough to check only those cases, where the given variable is present many times on the whole path *)

(* there are possibly multiple refinement paths *)
Scan[
Function[path, (*path is {{names...},{guards...},{actions...}}*)

Module[
{
eventNames=path[[1]],
inheritedGuards=path[[2]],
combinedActions=path[[3]],
combinedPromises=path[[4]],
pathKnowns,
suspectedVariables, (* variables modified differently on the refinement path *)
superposition (* correctness condition: base actions are equivalent to these actions *)
},

pathKnowns=Join[knowns,inheritedGuards];

suspectedVariables=Keys[Select[CountsBy[combinedActions,First],#>1&]];

If[suspectedVariables≠{},

superposition=Map[
Function[varName,
Equal@@(Select[combinedActions,First[#]===varName&][[All,2]])
],
suspectedVariables
];

If[combinedPromises≠{},
(* there are promises in the refinement paths, check if they are fulfilled *)
If[showProofsOpt,
prettyProof[
If[Length[guardsActionPaths]==1,
(* title for single refinement path *)
"State superposition for event "<>name,(* title for multiple refinement paths *)
"State superposition via "<>prettyPath[eventNames]
],
Join[pathKnowns,superposition],combinedPromises]
];

res=doValidate[
And@@Join[pathKnowns,superposition],
And@@combinedPromises,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
],

(* there are no promises, check only the satisfiability of superposition *)
If[showProofsOpt,
prettyReachabilityProof[
If[Length[guardsActionPaths]==1,
(* title for single refinement path *)
"State superposition for event "<>name,(* title for multiple refinement paths *)
"State superposition via "<>prettyPath[eventNames]
],
Join[pathKnowns,superposition]]
];

res=satisfy[
And@@Join[pathKnowns,superposition],
theorems->theoremsOpt,
verbose->verboseOpt
]
],

(* there are no suspected variables - that is, either there are no references to common variables across the refinement path, or modifications of such variables are syntactically identical and were thus omitted as duplicates already
-> if there are no promises at this level, but there are some in base model, check the feasibility of actions with regard to base promises *)
If[promises=={}&&combinedPromises≠{},
With[
{
basePromisesUpdated=combinedPromises/.actions
},

If[showProofsOpt,
prettyReachabilityProof[
If[Length[guardsActionPaths]==1,
(* title for single refinement path *)
"State superposition for event "<>name,(* title for multiple refinement paths *)
"State superposition via "<>prettyPath[eventNames]
],
Join[pathKnowns,basePromisesUpdated]]
];

res=satisfy[
And@@Join[pathKnowns,basePromisesUpdated],
theorems->theoremsOpt,
verbose->verboseOpt
]
],

(* nothing to check, consider superposition to pass *)
res=True
]
];

If[showResult[res,verboseOpt],
If[Length[guardsActionPaths]==1,
(* report for single refinement path *)
Print["    state superposition: ",prettyResult[res]],
(* report for multiple refinement paths *)
Print["    state superposition via ",prettyPath[eventNames],": ",prettyResult[res]]
]
];

AppendTo[results,res]
]
],
guardsActionPaths
]
];

(* check convergence if this is a new event in a refining model,
or if the convergence was ordered explicitly *)

If[(StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["convergence",onlyPhaseOpt])&&
(* do not check if the model is not refining, unless it is explicitly on: *)
(base=!=Null||isConvergent[ev,False])&&
(* check only if event is from this model (not implicit from base): *)
MemberQ[thisModelEventNames,name]&&
(* do not check if event is refining, unless it is explicitly on: *)
isConvergent[ev,directlyRefinedEvents=={}]&&
(* and do not if the check is explicitly suppressed: *)
isConvergent[ev,True],

If[variants≠{},

variantsAreNatural=Function[v,Element[v,Integers]&&v≥0]/@variants[[All,2]];

If[showProofsOpt,
prettyProof["Variant limited for event "<>name,
knowns,variantsAreNatural]
];

res=doValidate[
And@@knowns,
And@@variantsAreNatural,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    variant limited: ",prettyResult[res]]
];

AppendTo[results,res];

variantsAreMonotonic=Function[v,(v/.actions)<v]/@variants[[All,2]];

If[showProofsOpt,
prettyProof["Variant monotonic for event "<>name,
knowns,Join[variants[[All,2]],{"\ndecreases with\n"},actions]]
];

res=doValidate[
And@@knowns,
And@@variantsAreMonotonic,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    variant monotonic: ",prettyResult[res]]
];

AppendTo[results,res],

(*there are no variants,treat it as an incomplete model*)If[showResult[Indeterminate,verboseOpt],
Print["    no variants defined: ",prettyResult[Indeterminate]]
];
AppendTo[results,Indeterminate]
]
];

(* check anticipation only if ordered explicitly *)

If[(StringMatchQ["events",onlyPhaseOpt]||
StringMatchQ["convergence",onlyPhaseOpt])&&
isAnticipated[ev],

If[variants≠{},

variantsAreNatural=Function[v,Element[v,Integers]&&v≥0]/@variants[[All,2]];

If[showProofsOpt,
prettyProof["Variant limited for event "<>name,
knowns,variantsAreNatural]
];

res=doValidate[
And@@knowns,
And@@variantsAreNatural,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    variant limited: ",prettyResult[res]]
];

AppendTo[results,res];

variantsAreNonGrowing=Function[v,(v/.actions)<=v]/@variants[[All,2]];

If[showProofsOpt,
prettyProof["Variant non-growing for event "<>name,
knowns,Join[variants[[All,2]],{"\ndecreases with\n"},actions]]
];

res=doValidate[
And@@knowns,
And@@variantsAreNonGrowing,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    variant non-growing: ",prettyResult[res]]
];

AppendTo[results,res],

(* there are no variants, treat it as an incomplete model *)If[showResult[Indeterminate,verboseOpt],
Print["    no variants defined: ",prettyResult[Indeterminate]]
];
AppendTo[results,Indeterminate]
]
]

]
]
],
events
]
];

(* validate deaclock freedom, if requested *)
(* both deadlockFree and deadlockFree[] forms are accepted *)

If[MemberQ[m,_deadlockFree|deadlockFree]&&
StringMatchQ["deadlock",onlyPhaseOpt],

If[verboseOpt=!=Total,
Print["Validating deadlock freedom."]
];

Module[
{
(* base guards are collected from all leaf events of the base model *)
allBaseGuards=allGuards[baseEvents],

(* "current" guards are collected from all leaf events of this model *)
allThisGuards=allGuards[events],

knowns,
res
},

knowns=Join[
baseAxiomExprs,axiomExprs,
baseInvariantExprs,invariantExprs,
If[allBaseGuards===True,{},{allBaseGuards}]
];

If[showProofsOpt,
prettyProof["Deadlock freedom",knowns,{allThisGuards}]
];

res=doValidate[
And@@knowns,
allThisGuards,
theoremsOpt,
methodOpt,parallelOpt,verboseOpt
];

If[showResult[res,verboseOpt],
Print["    deadlock freedom: ",prettyResult[res]]
];

AppendTo[results,res]
]
];

(* print summary of final results *)

counts=Counts[results];
Print["Summary:"];
If[Length[counts]==0,
Print["Nothing was checked."],

If[Length[counts]==1,
Print["All ",Length[results]," ",prettyResult[First[results]]],

Map[
Function[r, (* r is result->count *)
Print["    ",prettyResult[r[[1]]]," ",r[[2]]]
],
Normal[Counts[results]]
]
]
];
]

Examples

Basic examples

deduceStep[{A,B,C},{{A,B}->X,{B,C}->Y},verbose->True]

deduce[
{¬A∧B,A∨¬B},
standardRules,
finalTerms->{True,False}
]

deduce[
{1}, (* start with 1 *)
{{_}->(a|->2a)}, (* double everything *)
finalTerms->(x|->x>20) (* until above 20 *)
]

deduce[
{2,3}, (* start with 2 and 3 *)
{{_,_}->({a,b}|->a*b)}, (* multiply any two values *)
finalTerms->(x|->x>20) (* until above 20 *)
]

rules={{_}->(x|->Mod[3x,10])};
result=deduce[{1},rules,withTrace->True];Grid[result]

showSteps[result,rules]

(* is the sum of two positive values also positive? yes, always *)
validate[
a>0∧b>0,
a+b>0
]

(* is the sum of two positive values less than 100? not necessarily *)
validate[
a>0∧b>0,
a+b<100
]

(* is it possible for the sum of two positive values to be less than 100? yes *)
satisfy[
a>0∧b>0∧a+b<100
]

(* is it possible for the sum of two positive values to be negative? no *)
satisfy[
a>0∧b>0∧a+b<0
]

Known issues

This fails to answer the question:

validate[
r∈(Integers)&&a∈(Integers)&&b∈(Integers)&&a==b,

(r==a\[Implies](r≠b)==False)&&((r≠b)==False\[Implies]r==a)
]

... even though it can solve each part of the question separately:

validate[
r∈(Integers)&&a∈(Integers)&&b∈(Integers)&&a==b,
(r==a\[Implies](r≠b)==False)(* &&((r≠b)==False\[Implies]r==a) *)
]

validate[
r∈(Integers)&&a∈(Integers)&&b∈(Integers)&&a==b,
(* (r==a\[Implies](r≠b)==False)&& *)((r≠b)==False\[Implies]r==a) 
]

This fails to answer the question:

validate[
i∈Booleans&&r∈(Integers)&&b∈(Integers)&&
(i==False\[Implies]r==b)&&
(r==b\[Implies]i==False),

i==(r≠b)
]

... even though it can do so in the piecewise mode:

validatePiecewise[
i∈Booleans&&r∈(Integers)&&b∈(Integers)&&
(i==False\[Implies]r==b)&&
(r==b\[Implies]i==False),

i==(r≠b)
]

This fails to answer the question (rounded average of two integer numbers is within their range):

validate[
a∈(Integers)&&b∈(Integers)&&a<b,
a≤IntegerPart[(a+b)/2]≤b
]

However, small restructuring of the question allows it to prove correctly:

validate[
a∈(Integers)&&b∈(Integers)&&a<b,
a≤a+IntegerPart[(b-a)/2]≤b
]

Some real problems can lead to expressions that are too difficult for the underlying functions to solve.
For example (see theorem “th1” in “Model - digital circuit: arbiter” example below):

expr1=(r2≠b2)==(r2≠a2);
expr2=((r2==b2&&r2==a2)||(r2!=b2&&r2!=a2));
FindInstance[
env≠cir&&
(mode==env||mode==cir)&&
r1∈(Integers)&&r1≥0&&
r2∈(Integers)&&r2≥0&&
a1∈(Integers)&&a1≥0&&
a2∈(Integers)&&a2≥0&&
a1≤r1&&r1≤1+a1&&a2≤r2&&r2≤1+a2&&
p1∈Booleans&&
p2∈Booleans&&
(p1==False||p2==False)&&
(mode==env\[Implies](p1==False\[Implies]r1==a1))&&
(mode==env\[Implies](p2==False\[Implies]r2==a2))&&
b1∈(Integers)&&b1≥0&&
o1∈Booleans&&
b2∈(Integers)&&b2≥0&&
o2∈Booleans&&
mode==cir&&

expr1 (* replace with equivalent expr2 *)
,
{a1,a2,b1,b2,cir,env,mode,o1,o2,p1,p2,r1,r2}
]

Source Code Verification

Mean value - naive version

This example demonstrates basic verification for a function that computes the mean of two integers.

int mean(int a, int b)
{
     int res = (a + b) / 2;
     
     return res;
}

The only “dangerous” operation is addition a+b, which can potentially overflow.

Initial assumptions (on a system with 32-bit integers):

intMin=-(2^31);
intMax=(2^31)-1;

Validate the lack of integer overflow in the addition:

validate[
intMin≤a≤intMax∧intMin≤b≤intMax,

intMin≤a+b≤intMax (* is it always the case? *)
]

This result shows that safe execution is not guaranteed.

We can assume that input values are limited by the caller, for example in the range 0..100. Then, the naive way to compute the mean value is safe:

validate[
0≤a≤100∧0≤b≤100,

a+b≤intMax (* and now, is it safe? *)
]

This result shows that if input values are in the range 0..100, then the mean value can be safely computed with this method - but for unconstrained inputs this method is not appropriate.

Mean value - corrected

We can notice that a+b does not lead to overflow if a and b have different signs - their sum is always somewhere between them. The overflow is avoided in that case.
We can also notice that instead of using the original formula, we can take one of two values and add to it half of their difference:

FullSimplify[((a+b)/2)==a+((b-a)/2)]

If a and b have the same sign, this method also avoids the overflow.

These observations suggest the following correct implementation:

int mean(int a, int b)
{
	int res;
	
	if ((a >= 0 && b >= 0) || (a < 0 && b < 0))
	{
		// a and b have the same sign
		
		res = a + (b - a) / 2;
	}
	else
	{
		// a and b have different signs
		
		res = (a + b) / 2;
	}
	
	return res;
}

The first branch has two potentially dangerous (leading to overflow) operations - subtraction and addition. The second branch has only one addition to check.

In the first branch, subtraction is safe:

validate[
(* what we know about variable a: *)
a∈Integers∧intMin≤a≤intMax∧

(* what we know about variable b: *)
b∈Integers∧intMin≤b≤intMax∧

(* condition of the first branch: *)
((a≥0∧b≥0)∨(a<0∧b<0)),

(* our verification condition: *)
intMin≤b-a≤intMax
]

Addition in the first branch is also safe:

validate[
(* what we know about variable a: *)
a∈Integers∧intMin≤a≤intMax∧

(* what we know about variable b: *)
b∈Integers∧intMin≤b≤intMax∧

(* condition of the first branch: *)
((a≥0∧b≥0)∨(a<0∧b<0)),

(* our verification condition: *)
intMin≤a+((b-a)/2)≤intMax
]

Finally, addition in the second branch (before dividing by half) is also fine:

validate[
(* what we know about variable a: *)
a∈Integers∧intMin≤a≤intMax∧

(* what we know about variable b: *)
b∈Integers∧intMin≤b≤intMax∧

(* condition of the second branch: *)
¬((a≥0∧b≥0)∨(a<0∧b<0)),

(* our verification condition: *)
intMin≤a+b≤intMax
]

Last but not least - the conditional statement (with two branches) was introduced in this version and it is prudent to check whether those branches are reachable - that is, whether it is possible to have the input values such that those branches are executed.

satisfy[
(* what we know about variable a: *)
a∈Integers∧intMin≤a≤intMax∧

(* what we know about variable b: *)
b∈Integers∧intMin≤b≤intMax∧

(* condition of the first branch: *)
((a≥0∧b≥0)∨(a<0∧b<0))
]

satisfy[
(* what we know about variable a: *)
a∈Integers∧intMin≤a≤intMax∧

(* what we know about variable b: *)
b∈Integers∧intMin≤b≤intMax∧

(* condition of the second branch: *)
¬((a≥0∧b≥0)∨(a<0∧b<0))
]

Event-B verification checks

All verification checks are demonstrated here in isolation.
Realistic models (see below) undergo (and sometimes fail) multiple checks at a time.

Initialization

Check the initial values against invariants - is the initial state legal?

good=model[
invariant["inv",a>0], (* a must be positive *)
init["init",a->42] (* and it is *)
];
bad=model[
invariant["inv",a>0], (* a must be positive *)
init["init",a->-42] (* but it is not *)
];

validateModel[good]

validateModel[bad]

Guard reachability

Check if the event can be executed at all - that is, if the conditions needed by the event guard are possible, even potentially.

good=model[
invariant["inv",a>0], (* a must be positive *)
event["ev",
when[a<42, (* it might happen one day *)
Null
]
]
];
bad=model[
invariant["inv",a>0], (* a must be positive *)
event["ev",
when[a<-42, (* it can never happen *)
Null
]
]
];

validateModel[good,onlyPhase->"guards"]

validateModel[bad,onlyPhase->"guards"]

Invariant preservation

Check if the event actions leave the system in a state that is still legal with regard to invariants.

good=model[
invariant["inv",a>0], (* a must be positive *)
event["ev",
a->42 (* still OK *)
]
];
bad=model[
invariant["inv",a>0], (* a must be positive *)
event["ev",
a->-42 (* not OK *)
]
];

validateModel[good,onlyPhase->"invariants"]

validateModel[bad,onlyPhase->"invariants"]

Deadlock freedom

Check if, assuming invariants, any of the events can take place. This is similar to guard reachability, but considers all events at once, not each of them in isolation.
The deadlock freedom check is optional (because it does not make sense in all systems) and has to be requested in the model by a separate flag.

good=model[
event["ev1",
when[a<42,
Null
]
],
event["ev2",
when[a>=42, (* OK, together with ev1 all possible states are covered *)
Null
]
],
deadlockFree[] (* this is how the deadlock check is switched on *)
];
bad=model[
event["ev1",
when[a<42, (* oops... *)
Null
]
],
event["ev2",
when[a>42, (* ...oops, what if a==42? *)
Null
]
],
deadlockFree[] (* this is how the deadlock check is switched on *)
];

validateModel[good,onlyPhase->"deadlock"]

validateModel[bad,onlyPhase->"deadlock"]

Initialization refinement

This applies to refined models.
New initializations cannot conflict with base model. Base initializations cannot conflict with new invariants, even if they were correct in the base model.

base=model[
invariant["inv",a>0], (* a must be positive *)
init["init",a->42] (* and it is *)
];
goodRefinement=model[
refines[base],
invariant["inv1",a>10] (* OK, more constrained, but base inits are still OK *)
];
badRefinement1=model[
refines[base],
invariant["inv1",a>100] (* oops, the base initial state does not fit any more *)
];
badRefinement2=model[
refines[base],
init["init2",a->7] (* oops, incompatible with base initialization *)
];

validateModel[goodRefinement,onlyPhase->"init"]

validateModel[badRefinement1,onlyPhase->"init"]

validateModel[badRefinement2,onlyPhase->"init"]

Refined guard reachability

This applies to refined models.
The refined guard can be stronger than the base one, but it still needs to be potentially reachable.

base=model[
invariant["inv",a>0], (* a must be positive *)
event["ev",
when[a<42,
Null
]
]
];
goodRefinement=model[
refines[base],
event["ev",
when[a<10, (* OK, stronger than in base model, but still possible *)
Null
]
]
];
badRefinement=model[
refines[base],
event["ev",
when[a<-10, (* oops, stronger than in base model and impossible to satisfy *)
Null
]
]
];

validateModel[goodRefinement,onlyPhase->"guards"]

validateModel[badRefinement,onlyPhase->"guards"]

Refined guard strengthening

This check applies to refined models.
The refined guard can be stronger than the base one, but not looser.

base=model[
event["ev",
when[a<42,
Null
]
]
];
goodRefinement=model[
refines[base],
event["ev",
when[a<10, (* OK, stronger than in base model *)
Null
]
]
];
badRefinement=model[
refines[base],
event["ev",
when[a<100, (* oops, looser than in base model *)
Null
]
]
];

validateModel[goodRefinement,onlyPhase->"guards"]

validateModel[badRefinement,onlyPhase->"guards"]

Refined promise strengthening

This check applies to refined models and is done together with guard check.
The refined promise can be stronger than the base one, but not looser.

base=model[
event["ev",a>42]
];
goodRefinement=model[
refines[base],
event["ev",a>100] (* OK, stronger promise *)
];
badRefinement=model[
refines[base],
event["ev",a>10] (* oops, looser promise *)
];

validateModel[goodRefinement,onlyPhase->"guards"]

validateModel[badRefinement,onlyPhase->"guards"]

Merging guard strengthening

This check applies to refined models, where new event refines multiple events from the base model.
The refined guard can be stronger than the disjunction of base ones, but not looser.

base=model[
event["ev1",
when[0<a<42,
Null
]
],
event["ev2",
when[42<=a<100,
Null
]
]
];
goodRefinement=model[
refines[base],
event["ev3"->{"ev1","ev2"}, (* merges two events from base model *)
when[0<a<100, (* same or stronger than both bases together *)
Null
]
]
];
badRefinement=model[
refines[base],
event["ev3"->{"ev1","ev2"}, (* merges two events from base model *)
when[0<a<=100, (* oops, 100 is not covered by any of the base events *)
Null
]
]
];

validateModel[goodRefinement,onlyPhase->"guards"]

validateModel[badRefinement,onlyPhase->"guards"]

Invariant compatibility

This applies to refined models.
Actions from base events have to be compatible with new invariants and actions from refined events have to be compatible with both base and new invariants.

base=model[
invariant["inv1",a>0], (* a must be positive *)
invariant["inv2",b>0], (* b must be positive, too *)
event["ev",
a->42
]
];
goodRefinement=model[
refines[base],
invariant["inv3",a<100], (* together with inv1, 0 < a < 100 *)
event["ev",
b->42
]
];
badRefinement1=model[
refines[base],
invariant["inv3",a<10], (* oops, together with inv1, 0 < a < 10 *)
event["ev",
b->42 (* this is OK, but base action now does not fit inv3 *)
]
];
badRefinement2=model[
refines[base],
event["ev",
b->-42 (* oops, conflicts with inv2 in base *)
]
];

validateModel[goodRefinement,onlyPhase->"invariants"]

validateModel[badRefinement1,onlyPhase->"invariants"]

validateModel[badRefinement2,onlyPhase->"invariants"]

State superposition

This applies to refined models.
Actions from base and refining events have to be compatible with regard to modifications of the same variables.

base=model[
event["ev",
{
a->42,
b->10
}
]
];
goodRefinement=model[
refines[base],
event["ev",
{
b->10, (* modification that is common for both base and refining event *)
c->100
}
]
];
badRefinement=model[
refines[base],
event["ev",
{
b->12, (* oops, incompatible modification *)
c->100
}
]
];

validateModel[goodRefinement,onlyPhase->"events"]

validateModel[badRefinement,onlyPhase->"events"]

State superposition over base promise

This applies to refined models.
Actions have to be compatible also with promises from base model, if the promise disappears in concrete event.

base=model[
event["ev",a>42] (* abstract promise that a > 42 *)
];
goodRefinement=model[
refines[base],
event["ev",a->100] (* OK, concrete action fits the base promise *)
];
badRefinement=model[
refines[base],
event["ev",a->10] (* oops, concrete action does not fit the base promise *)
];

validateModel[goodRefinement,onlyPhase->"superposition"]

validateModel[badRefinement,onlyPhase->"superposition"]

Event convergence

This applies to refined models.
New events that do not refine events from base model, should not starve existing events by “executing” forever - variants need to be used to demonstrate that the execution sequence of new events is limited.

base=model[
event["ev",Null]
];
goodRefinement1=model[
refines[base],
invariant["inv1",{a∈Integers,a<=10}],
invariant["inv2",{b∈Integers}],
variant["var1",10-a], (* this expression decreases when ev1 executes *)

event["ev1", (* this new event is implicitly convergent *)
when[a<10,
{
a->a+1
}
]
],
event["ev2", (* this new event has no impact on "a" (and on variant) *)
anticipated,
when[b<100,
{
b->b+1
}
]
]
];
badRefinement=model[
refines[base],
event["ev1",
when[a>10, (* oops, this might run forever *)
{
a->a+1
}
]
]
];
goodRefinement2=model[
refines[base],
event["ev1",
!convergent, (* we explicitly say it is acceptable ... *)
when[a>10, (* ... for this to run forever *)
{
a->a+1
}
]
]
];

validateModel[goodRefinement1,onlyPhase->"convergence"]

validateModel[badRefinement,onlyPhase->"convergence"]

validateModel[goodRefinement2,onlyPhase->"convergence"]

Model - cars on a bridge

This example is based on chapter 2 of the “Modeling in Event-B” book by Jean-Raymond Abrial.

Requirements

reqs=<|
"FUN-1"->"The system is controlling cars on a bridge connecting the mainland to an island.",
"ENV-1"->"The system is equipped with two traffic lights with two colors: green and red.",
"ENV-2"->"The traffic lights control the entrance to the bridge at both ends of it.",
"ENV-3"->"Cars are not supposed to pass on a red traffic light, only on a green one.",
"ENV-4"->"The system is equipped with four sensors with two states: on or off.",
"ENV-5"->"The sensors are used to detect the presence of a car entering or leaving the bridge: \"on\" means that a car is willing to enter the bridge or to leave it.",
"FUN-2"->"The number of cars on bridge and island is limited.",
"FUN-3"->"The bridge is one-way or the other, not both at the same time."
|>;

Initial attempt

myModel0=model[
axiom["axm0_1",{d∈Integers}], (* what we know about bridge and island capacity *)

invariant["inv0_1",{n∈Integers}], (* number of cars is always int *)
invariant["inv0_2",n≤d], (* cars on the bridge/island do not exceed capacity *)

event["ML_out", (* event for a car moving out to the bridge and island *)
n->n+1
],

event["ML_in", (* event for a car moving back from the bridge and island *)
n->n-1
]
];

validateModel[myModel0]

The init and ML_out events cannot be validated, because there are not enough details in the model.

Adding event guards

myModel0=model[
axiom["axm0_1",d∈Integers],
invariant["inv0_1",n∈Integers],
invariant["inv0_2",n≤d],

event["ML_out",
when[n<d, (* guard: there is space left on the bridge and island *)
n->n+1
]
],

event["ML_in",
when[0<n, (* guard: there is at least one car on the bridge and island *)
n->n-1
]
]
];

validateModel[myModel0]

Still, axioms cannot be validated, there is not enough data related to constant d, which expresses the capacity of the bridge and island.

Adding more axioms and init event

myModel0=model[
axiom["axm0_1",d∈Integers],
axiom["axm0_2", d>0], (* new axiom that allows the traffic to exist *)

init["init0",n->0], (* initial state *)

invariant["inv0_1",n∈Integers],
invariant["inv0_2",n≤d],

event["ML_out",when[n<d,n->n+1]],
event["ML_in",when[0<n,n->n-1]]
];

validateModel[myModel0]

Adding deadlock freedom requirement

reqs["FUN-4"]="Once started, the system should work for ever.";

myModel0=model[
axiom["axm0_1",d∈Integers],
axiom["axm0_2", d>0],

init["init0",n->0],

invariant["inv0_1",n∈Integers],
invariant["inv0_2",n≤d],

event["ML_out",when[n<d,n->n+1]],
event["ML_in",when[0<n,n->n-1]],

deadlockFree[] (* deadlock-freedom validation request *)
];

validateModel[myModel0]

First refinement

The refinement means that new, more precise model is based on (and is compatible with) a previous, more abstract model.

myModel1=model[
refines[myModel0], (* refinement relation *)

(* a is cars on the bridge moving to island *)
(* b is cars on island *)
(* c is cars on the bridge coming back from island *)
init["init1",{a->0,b->0,c->0}],

invariant["inv1_1",{a∈Integers,a≥0}],
invariant["inv1_2",{b∈Integers,b≥0}],
invariant["inv1_3",{c∈Integers,c≥0}],
invariant["inv1_4",a+b+c==n], (* n exists in base model *)
invariant["inv1_5",a==0||c==0], (* bridge is one-way *)

(* always decreasing variant for new events ensures that new events do not starve the events from base model (that is, new events cannot form infinite chains) *)
variant["variant1",2a+b],

event["ML_in",when[0<c,c->c-1]], (* refined base event *)
event["ML_out",when[{a+b<d,c==0},a->a+1]], (* refined base event *)
event["IL_in",when[0<a,{a->a-1,b->b+1}]], (* new event *)
event["IL_out",when[{b>0,a==0},{b->b-1,c->c+1}]], (* new event *)

deadlockFree[] (* deadlock-freedom validation request *)
];

validateModel[myModel1]

Second refinement, adding traffic lights

This refinement introduces traffic lights to control the way cars move between zones mainland-bridge-island.

color={green,red};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel2=model[
refines[myModel1],

axiom["amx2_2",uniqueElements[color]],

init["init2_0",{mlTl->red,ilTl->red}], (* not present in the book (!) *)

(* new invariants for traffic lights *)
invariant["inv2_1",mlTl∈color], (* mainland traffic light *)
invariant["inv2_2",ilTl∈color], (* island traffic light *)
invariant["inv2_3",mlTl==green\[Implies]a+b<d&&c==0],
invariant["inv2_4",ilTl==green\[Implies]b>0&&a==0],

event["ML_out", (* refinement *)
when[mlTl==green,
a->a+1
]
],
event["IL_out", (* refinement *)
when[ilTl==green,
{b->b-1,c->c+1}
]
],
event["ML_tl_green", (* new event - turn green for cars moving to island *)
when[{mlTl==red,a+b<d,c==0},
mlTl->green
]
],
event["IL_tl_green", (* new event - turn green for cars moving from islan *)
when[{ilTl==red,b>0,a==0},
ilTl->green
]
],

(* as in base model, but still needed here for completeness *)
event["ML_in",when[0<c,c->c-1]],
event["IL_in",when[0<a,{a->a-1,b->b+1}]]
];

validateModel[myModel2]

The above model cannot be validated, because it misses invariants...

Second refinement, adding invariants

color={green,red};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel2=model[
refines[myModel1],

axiom["amx2_2",uniqueElements[color]],

init["init2_0",{mlTl->red,ilTl->red}],

(* new invariants for traffic lights *)
invariant["inv2_1",mlTl∈color], (* mainland traffic light *)
invariant["inv2_2",ilTl∈color], (* island traffic light *)
invariant["inv2_3",mlTl==green\[Implies]a+b<d&&c==0],
invariant["inv2_4",ilTl==green\[Implies]b>0&&a==0],

(* new invariant, both lights cannot be green at the same time: *)
invariant["inv2_5",mlTl==red||ilTl==red],

event["ML_out", (* refinement *)
when[mlTl==green,
a->a+1
]
],
event["IL_out", (* refinement *)
when[ilTl==green,
{b->b-1,c->c+1}
]
],
event["ML_tl_green", (* new event - turn green for cars moving to island *)
when[{mlTl==red,a+b<d,c==0},
{
mlTl->green,
ilTl->red (* corrected action for inv2_5 *)
}
]
],
event["IL_tl_green", (* new event - turn green for cars moving from islan *)
when[{ilTl==red,b>0,a==0},
{
ilTl->green,
mlTl->red (* corrected action for inv2_5 *)
}
]
],

(* as in base model, but still needed here for completeness *)
event["ML_in",when[0<c,c->c-1]],
event["IL_in",when[0<a,{a->a-1,b->b+1}]]
];

validateModel[myModel2]

This model is still not complete, because ML_out and Il_out have to be split to conditionally turn their respective lights to red. This means that the split event will have disjoint guards...

Second refinement, splitting events

color={green,red};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel2=model[
refines[myModel1],

axiom["amx2_2",uniqueElements[color]],

init["init2_0",{mlTl->red,ilTl->red}],

(* new invariants for traffic lights *)
invariant["inv2_1",mlTl∈color], (* mainland traffic light *)
invariant["inv2_2",ilTl∈color], (* island traffic light *)
invariant["inv2_3",mlTl==green\[Implies]a+b<d&&c==0],
invariant["inv2_4",ilTl==green\[Implies]b>0&&a==0],
invariant["inv2_5",mlTl==red||ilTl==red], (* no two greens at the same time *)

event["ML_out_1"->"ML_out", (* split, but still refinement *)
when[{
mlTl==green,
a+b+1≠d (* additional condition in guard *)
},
a->a+1
]
],
event["ML_out_2"->"ML_out", (* split, but still refinement *)
when[{
mlTl==green,
a+b+1==d (* additional condition in guard *)
},
{
a->a+1,
mlTl->red
}
]
],
event["IL_out_1"->"IL_out", (* split, but still refinement *)
when[{
ilTl==green,
b≠1 (* additional condition in guard *)
},
{b->b-1,c->c+1}
]
],
event["IL_out_2"->"IL_out", (* split, but still refinement *)
when[{
ilTl==green,
b==1 (* additional condition in guard *)
},
{
b->b-1,c->c+1,
ilTl->red
}
]
],
event["ML_tl_green", (* new event - turn green for cars moving to island *)
when[{mlTl==red,a+b<d,c==0},
{
mlTl->green,
ilTl->red (* corrected action for inv2_5 *)
}
]
],
event["IL_tl_green", (* new event - turn green for cars moving from islan *)
when[{ilTl==red,b>0,a==0},
{
ilTl->green,
mlTl->red (* corrected action for inv2_5 *)
}
]
],

(* as in base model, but still needed here for completeness *)
event["ML_in",when[0<c,c->c-1]],
event["IL_in",when[0<a,{a->a-1,b->b+1}]]
];

validateModel[myModel2]

This model still needs to be completed with variants, to ensure that new events (those that are not refinements of events from base model) do not starve the old ones...

Second refinement, adding boolean variants

color={green,red};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

(* helper function for counting boolean values, for proving bool variants *)
boolCount[a_]:=If[a==True,1,0]
boolCount[a_,b_]:=boolCount[a]+boolCount[b]

myModel2=model[
refines[myModel1],

axiom["amx2_2",uniqueElements[color]],

init["init2_0",{
mlTl->red,ilTl->red,
mlPass∈Booleans,mlPass->True,ilPass∈Booleans,ilPass->True  (* new initial values for variants *)
}],

(* new invariants for traffic lights *)
invariant["inv2_1",mlTl∈color], (* mainland traffic light *)
invariant["inv2_2",ilTl∈color], (* island traffic light *)
invariant["inv2_3",mlTl==green\[Implies]a+b<d&&c==0],
invariant["inv2_4",ilTl==green\[Implies]b>0&&a==0],
invariant["inv2_5",mlTl==red||ilTl==red], (* no two greens at the same time *)

invariant["inv2_6",mlPass∈Booleans],
invariant["inv2_7",ilPass∈Booleans],

invariant["inv2_8",mlTl==red\[Implies]mlPass==True],
invariant["inv2_9",ilTl==red\[Implies]ilPass==True],

(* variant for new events *)
variant["variant_2",boolCount[mlPass,ilPass]],

event["ML_out_1"->"ML_out", (* split, but still refinement *)
when[{
mlTl==green,
a+b+1≠d (* additional condition in guard *)
},
{
a->a+1,
mlPass->True (* new variant change *)
}
]
],
event["ML_out_2"->"ML_out", (* split, but still refinement *)
when[{
mlTl==green,
a+b+1==d (* additional condition in guard *)
},
{
a->a+1,
mlTl->red,
mlPass->True(* new variant change *)
}
]
],
event["IL_out_1"->"IL_out", (* split, but still refinement *)
when[{
ilTl==green,
b≠1 (* additional condition in guard *)
},
{
b->b-1,c->c+1,
ilPass->True
}
]
],
event["IL_out_2"->"IL_out", (* split, but still refinement *)
when[{
ilTl==green,
b==1 (* additional condition in guard *)
},
{
b->b-1,c->c+1,
ilTl->red,
ilPass->True
}
]
],
event["ML_tl_green", (* new event - turn green for cars moving to island *)
when[
{
mlTl==red,a+b<d,c==0,
ilPass==True
},
{
mlTl->green,
ilTl->red ,
mlPass->False
}
]
],
event["IL_tl_green", (* new event - turn green for cars moving from island *)
when[
{
ilTl==red,b>0,a==0,
mlPass==True
},
{
ilTl->green,
mlTl->red,
ilPass->False
}
]
],

(* as in base model, but still needed here for completeness *)
event["ML_in",when[0<c,c->c-1]],
event["IL_in",when[0<a,{a->a-1,b->b+1}]],

deadlockFree[] (* deadlock-freedom validation request *)
];

validateModel[myModel2]

Third refinement, adding car sensors

reqs["FUN-5"]="The controller must be fast enough so as to be able to treat all the information coming from the environment.";

color={green,red};
sensor={On,Off};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

(* helper function for counting boolean values, for proving bool variants *)
boolCount[a_]:=If[a==True,1,0]
boolCount[a_,b_,c_,d_]:=boolCount[a]+boolCount[b]+boolCount[c]+boolCount[d]
sensorCount[a_]:=If[a==On,1,0]
sensorCount[a_,b_,c_,d_]:=sensorCount[a]+sensorCount[b]+sensorCount[c]+sensorCount[d]

myModel3=model[
refines[myModel2],

axiom["axm3_2",uniqueElements[sensor]],

(* initial values for new invariants *)
init["init3_0",{
mlOutSr->Off,mlInSr->Off,ilOutSr->Off,ilInSr->Off,
mlOut10∈Booleans,mlOut10->False,
mlIn10∈Booleans,mlIn10->False,
ilOut10∈Booleans,ilOut10->False,
ilIn10∈Booleans,ilIn10->False,
A->0,B->0,C->0
}],

(* new invariants for car sensors *)
invariant["inv3_1",mlOutSr∈sensor], (* mainland-to-bridge car sensor *)
invariant["inv3_2",mlInSr∈sensor], (* bridge-to-mainland car sensor *)
invariant["inv3_3",ilOutSr∈sensor], (* island-to-bridge car sensor *)
invariant["inv3_4",ilInSr∈sensor], (* bridge-to-island car sensor *)
invariant["inv3_5",{A∈Integers,A≥0}], (* physical num of cars going to island *)
invariant["inv3_6",{B∈Integers,B≥0}], (* physical num of cars on island *)
invariant["inv3_7",{C∈Integers,C≥0}], (* phys num of cars going to mainland *)

invariant["inv3_8",mlOut10∈Booleans],
invariant["inv3_9",mlIn10∈Booleans],
invariant["inv3_10",ilOut10∈Booleans],
invariant["inv3_11",ilIn10∈Booleans],

(* if the car is on sensor, then the physical num of cars in that group is positive: *)
invariant["inv3_12", ilInSr==On\[Implies]A>0],
invariant["inv3_13", ilOutSr==On\[Implies]B>0],
invariant["inv3_14", mlInSr==On\[Implies]C>0],

(* cars leave sensors (the sensor switches from 1 to 0) only when they have green light (they obey trafficl rules): *)
invariant["inv3_15",mlOut10==True\[Implies]mlTl==green],
invariant["inv3_16",ilOut10==True\[Implies]ilTl==green],

(* there are no messages from sensor as long as the car is above it: *)
invariant["inv3_17",ilInSr==On\[Implies]ilIn10==False],
invariant["inv3_18",ilOutSr==On\[Implies]ilOut10==False],
invariant["inv3_19",mlInSr==On\[Implies]mlIn10==False],
invariant["inv3_20",mlOutSr==On\[Implies]mlOut10==False],

(* controller's knowledge (a,b,c) is related to physical number of cars (A,B,C): *)
invariant["inv3_21",ilIn10==True&&mlOut10==True\[Implies]A==a],
invariant["inv3_22",ilIn10==False&&mlOut10==True\[Implies]A==a+1],
invariant["inv3_23",ilIn10==True&&mlOut10==False\[Implies]A==a-1],
invariant["inv3_24",ilIn10==False&&mlOut10==False\[Implies]A==a],
invariant["inv3_25",ilIn10==True&&ilOut10==True\[Implies]B==b],
invariant["inv3_26",ilIn10==True&&ilOut10==False\[Implies]B==b+1],
invariant["inv3_27",ilIn10==False&&ilOut10==True\[Implies]B==b-1],
invariant["inv3_28",ilIn10==False&&ilOut10==False\[Implies]B==b],
invariant["inv3_29",ilOut10==True&&mlIn10==True\[Implies]C==c],
invariant["inv3_30",ilOut10==True&&mlIn10==False\[Implies]C==c+1],
invariant["inv3_31",ilOut10==False&&mlIn10==True\[Implies]C==c-1],
invariant["inv3_32",ilOut10==False&&mlIn10==False\[Implies]C==c],

(* one-way bridge and limited number of cars on island hold for physical number, too: *)
invariant["inv3_33",A==0||C==0],
invariant["inv3_34",A+B+C≤d],

(* variant for new events *)
variant["variant_3",12-(sensorCount[mlOutSr,mlInSr,ilOutSr,ilInSr]+2*boolCount[mlOut10,mlIn10,ilOut10,ilIn10])],

event["ML_out_1",
when[{
mlOut10==True, (* new guard, wait for message from the sensor *)
a+b+1≠d
},
{
a->a+1,
mlPass->True,
mlOut10->False (* message from the sensor is considered to be consumed *)
}
]
],
event["ML_out_2",
when[{
mlOut10==True, (* new guard, wait for message from the sensor *)
a+b+1==d
},
{
a->a+1,
mlTl->red,
mlPass->True,
mlOut10->False (* message from the sensor is considered to be consumed *)
}
]
],
event["IL_out_1",
when[{
ilOut10==True, (* new guard, wait for message from the sensor *)
b≠1
},
{
b->b-1,c->c+1,
ilPass->True,
ilOut10->False (* message from the sensor is considered to be consumed *)
}
]
],
event["IL_out_2",
when[{
ilOut10==True,
b==1
},
{
b->b-1,c->c+1,
ilTl->red,
ilPass->True,
ilOut10->False (* message from the sensor is considered to be consumed *)
}
]
],

event["ML_in", (* refinement with the use of sensor message *)
when[
{
mlIn10==True,
0<c
},
{
c->c-1,
mlIn10->False
}
]
],
event["IL_in", (* refinement with the use of sensor message *)
when[
{
ilIn10==True,
0<a
},
{
a->a-1,b->b+1,
ilIn10->False
}
]
],

event["ML_tl_green", (* refinement with the use of sensor message *)
when[
{
mlTl==red,a+b<d,c==0,
ilPass==True,
ilOut10==False (* new guard, to ensure inv3_16 *)
},
{
mlTl->green,
ilTl->red ,
mlPass->False
}
]
],
event["IL_tl_green", (* refinement with the use of sensor message *)
when[
{
ilTl==red,b>0,a==0,
mlPass==True,
mlOut10==False (* new guard, to ensure inv3_15 *)
},
{
ilTl->green,
mlTl->red,
ilPass->False
}
]
],

(* new events representing cars arriving on sensors: *)
event["ML_out_arr",
when[
{
mlOutSr==Off,
mlOut10==False
},
mlOutSr->On
]
],
event["ML_in_arr",
when[
{
mlInSr==Off,
mlIn10==False,
C>0
},
mlInSr->On
]
],
event["IL_out_arr",
when[
{
ilOutSr==Off,
ilOut10==False,
B>0
},
ilOutSr->On
]
],
event["IL_in_arr",
when[
{
ilInSr==Off,
ilIn10==False,
A>0
},
ilInSr->On
]
],

(* new events representing cars leaving sensors: *)
event["ML_out_dep",
when[
{
mlOutSr==On,
mlTl==green
},
{
mlOutSr->Off,
mlOut10->True,
A->A+1
}
]
],
event["ML_in_dep",
when[
mlInSr==On,
{
mlInSr->Off,
mlIn10->True,
C->C-1
}
]
],
event["IL_out_dep",
when[
{
ilOutSr==On,
ilTl==green
},
{
ilOutSr->Off,
ilOut10->True,
B->B-1,
C->C+1
}
]
],
event["IL_in_dep",
when[
ilInSr==On,
{
ilInSr->Off,
ilIn10->True,
A->A-1,
B->B+1
}
]
],

deadlockFree[] (* deadlock-freedom validation request *)
];

(* Note: invariants "inv2_*" are troublemakers, which apparently cannot be solved with default Whole method.
The Piecewise method allows to solve the whole model; it "just works", but can take several hours to complete. The parallel option helps, too.

An alternative strategy is to divide the validation of invariants into two groups and use appropriate methods for most efficient solution.
This is left as an exercise to the user. :-)
 *)
validateModel[myModel3,method->Piecewise,parallel->True]

Model - mechanical press controller

This example is based on chapter 3 of the “Modeling in Event-B” book by Jean-Raymond Abrial.

Action and reaction pattern (weak)

This model has a weak synchronization guarantee, so that reactions do not have to follow all actions (that is, some actions can be missed).

myPattern0=model[
invariant["pat0_1",a∈{0,1}], (* action *)
invariant["pat0_2",r∈{0,1}], (* reaction *)
invariant["pat0_3",{ca∈Integers,ca≥0}], (* action counter is Natural *)
invariant["pat0_4",{cr∈Integers,cr≥0}], (* reaction counter is Natural *)
invariant["pat0_5",cr≤ca], (* there are at most ca reactions *)

(* try with and without this: *)
invariant["pat0_6",a==1&&r==0\[Implies]cr<ca],

init["init0",{a->0,r->0,ca->0,cr->0}], (* initially nothing happened *)

event["a_on", (* action happened *)
when[a==0,
{
a->1,
ca->ca+1
}
]
],
event["a_off", (* action dismissed *)
when[a==1,
a->0
]
],
event["r_on", (* reaction happened *)
when[{r==0,a==1},
{
r->1,
cr->cr+1
}
]
],
event["r_off", (* reaction dismissed *)
when[{r==1,a==0},
r->0
]
]
];

validateModel[myPattern0]

Refinement with retro-acting reaction (strong)

This refinement adds strong synchronization, so all actions are followed by reactions.

myPattern1=model[
refines[myPattern0], (* refinement of previous model *)

invariant["pat1_1",ca≤cr+1], (* actions can be at most one step ahead *)
invariant["pat1_2",a==0\[Implies]ca==cr], (* reactions follow up before action is off *)
invariant["pat1_3",a==1&&r==1\[Implies]ca==cr],

event["a_on",
when[{a==0,r==0},
{
a->1,
ca->ca+1
}
]
],
event["a_off",
when[{a==1,r==1},
a->0
]
]
];

validateModel[myPattern1]

Now the counters ca and cr can be removed from the model, because they were used only to guide the refinement. The a and r variables are sufficient (with proper guards) to maintain strong synchronization.

Requirements of the mechanical press

reqs=<|
"EQP-1"->"The system has got the following pieces of equipment: a motor, a clutch, and a door.",
"EQP-2"->"Four buttons are used to start and stop the motor, and engage and disengage the clutch.",
"EQP-3"->"A controller is supposed to manage these equipment.",
"FUN-1"->"Buttons and controller are weakly synchronized.",
"FUN-2"->"Controller and equipment are strongly synchronized.",
"SAF-1"->"When the clutch is engaged, the motor must work.",
"SAF-2"->"When the clutch is engaged, the door must be closed.",
"FUN-3"->"When the clutch is disengaged, the door cannot be closed several times, ONLY ONCE.",
"FUN-4"->"When the door is closed, the clutch cannot be disengaged several times, ONLY ONCE.",
"FUN-5"->"Opening and closing the door is not independent. It must be synchronized with disengaging and engaging the clutch."
|>;

Initial model: connecting the controller to the motor

The connections between components follow the action-reaction patterns above.

status={stopped,working};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel0=model[
axiom["axm0_1",uniqueElements[status]],

invariant["inv0_1",motorSensor∈status],
invariant["inv0_2",motorActuator∈status],

init["init0",{motorSensor->stopped,motorActuator->stopped}],

(* controller events: *)
event["treat_start_motor",
when[{motorActuator==stopped,motorSensor==stopped},
motorActuator->working
]
],
event["treat_stop_motor",
when[{motorActuator==working,motorSensor==working},
motorActuator->stopped
]
],

(* physical reaction of the motor: *)
event["Motor_start",
when[{motorSensor==stopped,motorActuator==working},
motorSensor->working
]
],
event["Motor_stop",
when[{motorSensor==working,motorActuator==stopped},
motorSensor->stopped
]
],

deadlockFree[]
];

validateModel[myModel0]

First refinement: connecting the motor buttons to the controller

myModel1=model[
refines[myModel0],

(* physical buttons (they motivate changes in controller variables) *)
invariant["inv1_1",stopMotorButton∈Booleans],
invariant["inv1_2",startMotorButton∈Booleans],

(* knowledge of physical status of the buttons *)
invariant["inv1_3",stopMotorImpulse∈Booleans],
invariant["inv1_4",startMotorImpulse∈Booleans],

init["init1",
{
stopMotorButton∈Booleans,stopMotorButton->False,
startMotorButton∈Booleans,startMotorButton->False,
stopMotorImpulse∈Booleans,stopMotorImpulse->False,
startMotorImpulse∈Booleans,startMotorImpulse->False
}
],

(* events representing operations on physical buttons *)
event["push_start_motor_button",
!convergent,
when[startMotorButton==False,startMotorButton->True]
],
event["release_start_motor_button",
!convergent,
when[startMotorButton==True,startMotorButton->False]
],

(* events representing the influence of buttons on what the controller knows *)
(* synchronization between physical button and the controller knowledge is weak *)
event["treat_push_start_motor_button"->"treat_start_motor",
!convergent,
when[
{
startMotorImpulse==False,
startMotorButton==True,
motorActuator==stopped, (* old guard *)
motorSensor==stopped (* old guard *)
},
{
startMotorImpulse->True,
motorActuator->working (* old action *)
}
]
],
event["treat_release_start_motor_button",
!convergent,
when[
{
startMotorImpulse==True,
startMotorButton==False
},
startMotorImpulse->False
]
],

(* additional "false" event to deal with superposition of patterns:
treat_push_start_motor_button was created on top of treat_start_motor and even though it properly strengthens the base guard, it is itself not completely covered if the base guard of treat_start_motor is false; the "false" event extends the overage of the higher pattern *)

event["treat_push_start_motor_button_false",
!convergent,
when[
{
startMotorImpulse==False,
startMotorButton==True,
Not[motorActuator==stopped&& (* false part of base guard *)
motorSensor==stopped ]
},
startMotorImpulse->True (* only "higher" action *)
]
],

(* similarly for stopping buttons and controls *)
event["push_stop_motor_button",
!convergent,
when[stopMotorButton==False,stopMotorButton->True]
],
event["release_stop_motor_button",
!convergent,
when[stopMotorButton==True,stopMotorButton->False]
],
event["treat_push_stop_motor_button"->"treat_stop_motor",
!convergent,
when[
{
stopMotorImpulse==False,
stopMotorButton==True,
motorSensor==working,
motorActuator==working
},
{
stopMotorImpulse->True,
motorActuator->stopped
}
]
],
event["treat_release_stop_motor_button",
!convergent,
when[
{
stopMotorImpulse==True,
stopMotorButton==False
},
stopMotorImpulse->False
]
],

event["treat_push_stop_motor_button_false",
!convergent,
when[
{
stopMotorImpulse==False,
stopMotorButton==True,
Not[motorActuator==working&&
motorSensor==working ]
},
stopMotorImpulse->True
]
],

deadlockFree[]
];

validateModel[myModel1]

Second refinement: connecting the controller to the clutch

clstatus={engaged,disengaged};

myModel2=model[
refines[myModel1],

axiom["axm2_1",uniqueElements[clstatus]],

(* clutch controller variables *)
invariant["inv2_1",clutchSensor∈clstatus],
invariant["inv2_2",clutchActuator∈clstatus],

(* physical buttons (they motivate changes in controller variables) *)
invariant["inv2_3",stopClutchButton∈Booleans],
invariant["inv2_4",startClutchButton∈Booleans],

(* knowledge of physical status of the buttons *)
invariant["inv2_5",stopClutchImpulse∈Booleans],
invariant["inv2_6",startClutchImpulse∈Booleans],

init["init2",
{
clutchSensor∈clstatus,clutchSensor->disengaged,
clutchActuator∈clstatus,clutchActuator->disengaged,
stopClutchButton∈Booleans,stopClutchButton->False,
startClutchButton∈Booleans,startClutchButton->False,
stopClutchImpulse∈Booleans,stopClutchImpulse->False,
startClutchImpulse∈Booleans,startClutchImpulse->False
}
],

(* events representing operations on physical buttons *)
event["push_start_clutch_button",
!convergent,
when[startClutchButton==False,startClutchButton->True]
],
event["release_start_clutch_button",
!convergent,
when[startClutchButton==True,startClutchButton->False]
],

(* events representing the influence of buttons on what the controller knows *)
(* Note: this event does not refine any base event (as was the case with the motor in myModel1), because both physical and control aspects are added in a single step *)
event["treat_push_start_clutch_button",
!convergent,
when[
{
startClutchImpulse==False,
startClutchButton==True,
clutchActuator==disengaged,
clutchSensor==disengaged 
},
{
startClutchImpulse->True,
clutchActuator->engaged
}
]
],
event["treat_release_start_clutch_button",
!convergent,
when[
{
startClutchImpulse==True,
startClutchButton==False
},
startClutchImpulse->False
]
],

(* additional "false" event to deal with superposition of patterns *)
event["treat_push_start_clutch_button_false",
!convergent,
when[
{
startClutchImpulse==False,
startClutchButton==True,
Not[clutchActuator==disengaged&& (* false part of base guard *)
clutchSensor==disengaged ]
},
startClutchImpulse->True (* only "higher" action *)
]
],

(* similarly for stopping buttons and controls *)
event["push_stop_clutch_button",
!convergent,
when[stopClutchButton==False,stopClutchButton->True]
],
event["release_stop_clutch_button",
!convergent,
when[stopClutchButton==True,stopClutchButton->False]
],
event["treat_push_stop_clutch_button",
!convergent,
when[
{
stopClutchImpulse==False,
stopClutchButton==True,
clutchSensor==working,
clutchActuator==working
},
{
stopClutchImpulse->True,
clutchActuator->disengaged
}
]
],
event["treat_release_stop_clutch_button",
!convergent,
when[
{
stopClutchImpulse==True,
stopClutchButton==False
},
stopClutchImpulse->False
]
],

event["treat_push_stop_clutch_button_false",
!convergent,
when[
{
stopClutchImpulse==False,
stopClutchButton==True,
Not[clutchActuator==engaged&&
clutchSensor==engaged ]
},
stopClutchImpulse->True
]
],

(* physical reaction of the clutch: *)
event["Clutch_start",
!convergent,
when[{clutchSensor==disengaged,clutchActuator==engaged},
clutchSensor->engaged
]
],
event["Clutch_stop",
!convergent,
when[{clutchSensor==engaged,clutchActuator==disengaged},
clutchSensor->disengaged
]
],

deadlockFree[]
];

validateModel[myModel2]

Another pattern: weak synchronization of two strong reactions

This pattern ensures that two reactions are strictly one-within-another in terms of time - that is, one (B) starts after the other (A) starts and it (B) finishes before the other (A) finishes. The coupling is weak in that the A “thing” can bounce up before the B “thing” starts and B can bounce down before A finishes.

The “outer thing” A has action a and reaction r, whereas the “inner thing” B has action b and reaction s.

The challenge is to couple these two patterns without modifying their reactive parts (r and s).

myPattern2=model[ (* this model contains both patterns, but independent (not coupled) *)

invariant["dbl0_1",a∈{0,1}],
invariant["dbl0_2",r∈{0,1}],
invariant["dbl0_3",{ca∈Integers,ca≥0}],
invariant["dbl0_4",{cr∈Integers,cr≥0}],
invariant["dbl0_5",a==1&&r==0\[Implies]ca==cr+1],
invariant["dbl0_6",a==0||r==1\[Implies]ca==cr],

invariant["dbl0_7",b∈{0,1}],
invariant["dbl0_8",s∈{0,1}],
invariant["dbl0_9",{cb∈Integers,cb≥0}],
invariant["dbl0_10",{cs∈Integers,cs≥0}],
invariant["dbl0_11",b==1&&s==0\[Implies]cb==cs+1],
invariant["dbl0_12",b==0||s==1\[Implies]cb==cs],

init["init0",{a->0,r->0,ca->0,cr->0,b->0,s->0,cb->0,cs->0}],

(* separate patterns for A (a/r) and B (b/s) *)

event["a_on",when[{a==0,r==0},{a->1,ca->ca+1}]],
event["a_off",when[{a==1,r==1},a->0]],
event["r_on",when[{r==0,a==1},{r->1,cr->cr+1}]],
event["r_off",when[{r==1,a==0},r->0]],
event["b_on",when[{b==0,s==0},{b->1,cb->cb+1}]],
event["b_off",when[{b==1,s==1},b->0]],
event["s_on",when[{s==0,b==1},{s->1,cs->cs+1}]],
event["s_off",when[{s==1,b==0},s->0]],

deadlockFree[]
];

validateModel[myPattern2]

myPattern3=model[ (* this model couples two patterns *)
refines[myPattern2],

(* the constraint that weakly couples both patterns from myPattern2 *)
invariant["dbl1_1",s==1\[Implies]r==1],

(* the following refinements for the coupling invariant above are sufficient for proper operation, but the challenge here is not to modify the events... *)
(*
event["s_on",when[{s==0,b==1,r==1},{s->1,cs->cs+1}]],
event["r_off",when[{r==1,a==0,s==0},r->0]]
*)

(* ... so we can modify the action events instead: *)
invariant["dbl1_2",b==1\[Implies]r==1], (* B's action happens after A's reaction *)
invariant["dbl1_3",a==0\[Implies]s==0], (* A's action goes down after B's reaction *)
event["b_on",
when[
{
b==0,
s==0,
r==1 ,a==1(* additional (constraining) guards *)
},
{b->1,cb->cb+1}
]
],
invariant["dbl1_4",a==0\[Implies]s==0], (* A's action goes down after B's reaction *)
invariant["dbl1_5",a==0\[Implies]b==0], (* to support dbl1_3 *)
event["a_off",
when[
{
a==1,
r==1,
s==0 ,b==0(* additional (constraining) guards *)
},
a->0
]
]
];

validateModel[myPattern3]

Third refinement: constraining the clutch and the motor

The application of the pattern above in the model is needed, because:

reqs["SAF-1"]

myModel3=model[
refines[myModel2],

invariant["inv3_1",clutchSensor==engaged\[Implies]motorSensor==working],
invariant["inv3_2",clutchActuator==engaged\[Implies]motorSensor==working],
invariant["inv3_3",motorActuator==stopped\[Implies]clutchSensor==disengaged],
invariant["inv3_4",motorActuator==stopped\[Implies]clutchActuator==disengaged],

event["treat_push_start_clutch_button", (* refinement *)
!convergent,
when[
{
startClutchImpulse==False,
startClutchButton==True,
clutchActuator==disengaged,
clutchSensor==disengaged,
motorSensor==working,(* additional (constraining) guard *)
motorActuator==working (* ditto *)
},
{
startClutchImpulse->True,
clutchActuator->engaged
}
]
],
event["treat_push_stop_motor_button", (* refinement *)
!convergent,
when[
{
stopMotorImpulse==False,
stopMotorButton==True,
motorActuator==working,
motorSensor==working,
clutchSensor==disengaged,(* additional (constraining) guard *)
clutchActuator==disengaged (* ditto *)
},
{
motorActuator->stopped,
stopMotorImpulse->True
}
]
]
];

validateModel[myModel3]

Fourth refinement: connecting the controller to the door

dstatus={open,closed};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel4=model[
refines[myModel3],

axiom["axm4_1",uniqueElements[dstatus]],

invariant["inv4_1",doorSensor∈dstatus],
invariant["inv4_2",doorActuator∈dstatus],

init["init4",{doorSensor->closed,doorActuator->closed}],

(*controller events:*)
event["treat_open_door",
!convergent,
when[{doorActuator==closed,doorSensor==closed},
doorActuator->open
]
],
event["treat_close_door",
!convergent,
when[{doorActuator==open,doorSensor==open},
doorActuator->closed
]
],
(*physical reaction of the door:*)
event["Door_open",
!convergent,
when[{doorSensor==closed,doorActuator==open},
doorSensor->open
]
],
event["Door_close",
!convergent,
when[{doorSensor==open,doorActuator==closed},
doorSensor->closed
]
]
];

validateModel[myModel4]

Fifth refinement: constraining the clutch and the door

Additional constraints due to the following existing requirement:

reqs["SAF-2"]

This has to be complemented with additional requirement:

reqs["SAF-3"]="When the motor is stopped, the door must be open.";

Then the pattern from 3rd refinement can be repeated for clutch and door:

myModel5=model[
refines[myModel4],

invariant["inv5_1",clutchSensor==engaged\[Implies]doorSensor==closed],
invariant["inv5_2",clutchActuator==engaged\[Implies]doorSensor==closed],
invariant["inv5_3",doorActuator==open\[Implies]clutchSensor==disengaged],
invariant["inv5_4",doorActuator==open\[Implies]clutchActuator==disengaged],

event["treat_push_start_clutch_button", (* refinement *)
!convergent,
when[
{
startClutchImpulse==False,
startClutchButton==True,
clutchActuator==disengaged,
clutchSensor==disengaged,
motorSensor==working,
motorActuator==working ,
doorSensor==closed,(* additional (constraining) guard *)
doorActuator==closed (* ditto *)
},
{
startClutchImpulse->True,
clutchActuator->engaged
}
]
],
event["treat_open_door", (* refinement *)
!convergent,
when[
{
doorActuator==closed,
doorSensor==closed,
clutchSensor==disengaged,(* additional (constraining) guard *)
clutchActuator==disengaged (* ditto *)
},
{
doorActuator->open
}
]
]
];

validateModel[myModel5,parallel->True]

Another pattern: strong synchronization of two strong reactions

reqs["FUN-4"]

This pattern ensures that two reactions are strictly one-within-another in terms of time - that is, one (B) starts after the other (A) starts and it (B) finishes before the other (A) finishes. The coupling is strong in that the A and B “things” can switch only once between each other.

The A “thing” has action a and reaction r, whereas the “thing” B has action b and reaction s.

The challenge is to couple these two patterns without modifying their reactive parts (r and s).

myPattern4=model[
refines[myPattern3],

(* m handles the "phase" of the cycle between A and B *)
invariant["dbl2_1",m∈{0,1}],
invariant["dbl2_2",m==1\[Implies]ca==cb+1],
invariant["dbl2_3",m==0\[Implies]ca==cb],
invariant["dbl2_4",r==1&&s==0&&(m==1||b==1)\[Implies]cr==cs+1],
invariant["dbl2_5",r==0||s==1||(m==0&&b==0)\[Implies]cr==cs],

invariant["dbl2_6",m==0\[Implies]a==0||r==1],
invariant["dbl2_7",m==1\[Implies]b==0&&s==0&&a==1],

init["init2",m->0],

event["a_on", (* refining *)
when[{a==0,r==0},
{
a->1,
ca->ca+1,
m->1 (* new action *)
}
]
],

event["b_on", (* refining *)
when[
{
b==0,s==0,r==1 ,a==1,
m==1 (* additional guard *)
},
{
b->1,
cb->cb+1,
m->0 (* additional action *)
}
]
],

event["a_off", (* refining *)
when[
{
a==1,r==1,s==0 ,b==0,
m==0 (* additional guard *)
},
a->0
]
],

deadlockFree[]
];

validateModel[myPattern4]

Sixth refinement: more constraints between clutch and door

This refinement applies strong-strong pattern over the 5th refinement.

myModel6=model[
refines[myModel5],

(* this invariant is copied from base models to support piecewise computation of deadlock freedom (it takes infinitely long without it) *)
invariant["inv6_4",startClutchButton∈Booleans],

(* again, variable m controls the "phase" of interaction *)

event["treat_close_door", (* refinement *)
!convergent,
when[
{
doorActuator==open,
doorSensor==open,
motorActuator==working,
motorSensor==working
},
{
doorActuator->closed,
m->1 (* additional action *)
}
]
],

event["treat_push_start_clutch_button", (* refinement *)
!convergent,
when[
{
startClutchImpulse==False,
startClutchButton==True,
clutchActuator==disengaged,
clutchSensor==disengaged,
motorSensor==working,
motorActuator==working ,
doorSensor==closed,
doorActuator==closed,
m==1 (* additional guard *)
},
{
startClutchImpulse->True,
clutchActuator->engaged,
m->0 (* additional action *)
}
]
],

event["treat_open_door", (* refinement *)
!convergent,
when[
{
doorActuator==closed,
doorSensor==closed,
clutchSensor==disengaged,
clutchActuator==disengaged,
m==0 (* additional guard *)
},
{
doorActuator->open
}
]
],

deadlockFree[]
];

(* this validates everything except the deadlock freedom *)
validateModel[myModel6,onlyPhase->"init"|"events"|"guards"|"invariants"|"superposition"|"convergence"]

(* this efficiently validates the deadlock freedom (which takes infinitely long with default method->Whole) *)
validateModel[myModel6,onlyPhase->"deadlock",method->Piecewise]

Template for simple inductive theorems

This template demonstrates how a simple theorem can be injected in the model validator.

Example:
- 0 is considered an even number
- any number that is +2 some other even number is also even

More formally, let even[x] be a statement about x being even, then:

Column[{even[0]==True,ForAll[x,x>0,even[x]\[Implies]even[x+2]]}]

(* template for simple (one-variable) inductive theorems *)
evenTheorem[knowns_,question_]:=Module[
{
knownEvens,
newKnowns,
newQuestion
},
knownEvens=Cases[{even[0],knowns},even[v_]:>v,{0,Infinity}];
newKnowns=DeleteCases[knowns,_even,{0,Infinity}];
newQuestion=question/.Map[
Function[qe, (* qe is even[...] *)
With[
{
v=qe[[1]] (* value tested, like in even[v] *)
},
qe->Or@@Map[ (* qe is replaced with Or-ed test against all known evens *)
Function[e, (* e is some known even value (including starting 0) *)
v==e||v==e+2 (* v is even, if equal to some known even or +2 *)
],
knownEvens
]
]
],
Cases[question,_even,{0,Infinity}]
];
{newKnowns,newQuestion}
]

Such a function can be provided as a hint to the model and will be used to pre-process the knowns and the question before the actual deduction.

The following model with invariant that a counter remains even based on the above inductive theorem can validate properly:

m=model[
theorem["th",evenTheorem], (* the evenTheorem applied to the model *)

invariant["inv",
{
n∈Integers,n≥0, (* counter *)
even[n]==True (* we want the counter to always remain even *)
}
],

init["init",{n->0}], (* counter is even at the beginning *)

event["ev",
when[n<1000,
{
n->n+2(* does the counter remain even all the time? *)
}
]
]
];

validateModel[m]

Model - simple file transfer protocol

This example is based on chapter 4 of the “Modeling in Event-B” book by Jean-Raymond Abrial.

Requirements

reqs=<|
"FUN-1"->"The protocol ensures the copy of a file from one site to another one.",
"FUN-2"->"The file is supposed to be made of a sequence of items.",
"FUN-3"->"The file is sent piece by piece between the two sites."
|>;

Initial model

The model assumes that file elements are transmitted sequentially, from the beginning to the end - it is not based on the notion of “partial function” on a given interval.
Constant f represents a file to be copied, variable g is a copied file that in this high-level view just transitions from “not copied” to “copied”.

myModel0=model[
axiom["axm0_1",{n∈Integers,n>0}],
axiom["axm0_2",{f∈Span,f==Span[1,n]}],

invariant["inv0_1",{b∈Booleans,g∈Span}],
invariant["inv0_2",{b==False\[Implies]g==∅}],
invariant["inv0_3",{b==True\[Implies]g==f}],

init["init0",
{
g->∅,
b∈Booleans,b->False
}
],

(* this is "fictional" event that allows to observe that the file was copied *)
event["final",
when[b==False,
{
g->f,
b->True
}
]
]
];

validateModel[myModel0]

First refinement

This refinement introduces variable h that represents the part of file that was already copied; the index r is one-past-the-end for that copied part. New event receive allows to “observe” the process of file transfer in more granularity.

myModel1=model[
refines[myModel0],

invariant["inv1_1",{r∈Span[1,n+1]}], (* file index *)
invariant["inv1_2",{h∈Span,h==Span[1,r-1]}], (* h ⊆ f *)
invariant["inv1_3",b==True\[Implies]r==n+1],

init["init1",
{
h∈Span, (* note: necessary for proper processing of the following *)
h->Span[1,0], (* ∅, but with lower bound already established *)
r->1
}
],

(* for event receive, which is limited by file size *)
variant["var1",n+1-r],

event["receive",
when[r<=n,
{
h->h+r, (* span h extends one element up *)
r->r+1
}
]
],

event["final", (* refining *)
when[
{
r==n+1, (* all elements copied *)
b==False
},
{
b->True
}
]
],

deadlockFree[]
];

validateModel[myModel1]

Second refinement

This refinement introduces even more granularity with new event send. The index s points to the element that was just sent. This model does not take into account the actual values of “transmitted” elements.

myModel2=model[
refines[myModel1],

invariant["inv2_1",{s∈Integers,s>0,s<=n+1}],
invariant["inv2_2",s∈Span[r,r+1]],
(* inv2_3 not used here *)

init["init2",s->1],

(* for event send, which is limited by file size *)
variant["var2",n+1-s],

event["send",
when[
{
s==r,
r!=n+1
},
s->s+1
]
],

event["receive", (* refining *)
when[s==r+1,
h->h+r,
r->r+1
]
]
];

validateModel[myModel2]

Third refinement

This refinement introduces parity counters and relies on two different theorems about parity to validate properly.

In the first theorem, parity[n,p] is a statement that p is a parity value (0 or 1) for number n. The inductive nature of this theorem is that:

Column[{parity[0,0]==True,ForAll[x,x>0,parity[x,p]\[Implies]parity[x+1,1-p]]}]

parityTheorem[knowns_,question_]:=Module[
{
knownParities,
newKnowns,
newQuestion
},
knownParities=Cases[{parity[0,0],knowns},parity[n_,p_]:>{n,p},{0,Infinity}];
newKnowns=DeleteCases[knowns,_parity,{0,Infinity}];
newQuestion=question/.Map[
Function[qp, (* qp is parity[...] in question *)
With[
{
n=qp[[1]], (* number *)
p=qp[[2]] (* parity *)
},
qp->Or@@Map[ (* qp is replaced with Or-ed test against all known parities *)
Function[knp, (* knp is some known {n,p} pair (including starting {0,0}) *)

(* p is a parity value of number n, if: *)
(n==knp[[1]]&&p==knp[[2]])|| (* we know it already, or ... *)
(n==knp[[1]]+1&&p==1-knp[[2]]) (* ... we can induce it *)
],
knownParities
]
]
],
Cases[question,_parity,{0,Infinity}]
];
{newKnowns,newQuestion}
]

The other theorem states that if two numbers differ from each other by at most 1, then if their parities are equal, the numbers are equal, too. This theorem applies to the send and receive counters and is injected directly in the model, without defining it as a separate function.

myModel3=model[
refines[myModel2],

(* theorems can be defined elsewhere and referred by name: *)
theorem["th3_1",parityTheorem],

(* very simple theorems can be injected directly, using the axiom mechanism: *)
axiom["th3_2",(p==q\[Implies]s==r)&&(p≠q\[Implies]s≠r)],

invariant["inv3_1", (* parity of send counter *)
{
p∈{0,1},
parity[s,p]==True
}
],
invariant["inv3_2",  (* parity of receive counter *)
{
q∈{0,1},
parity[r,q]==True
}
],

init["init3",{p->1,q->1}], (* because r->1 in myModel1 and s->1 in myModel2 *)

event["send",
when[
{
p==q, (* base guard (s==r) is strengthened *)
s!=n+1
},
{
s->s+1,
p->1-p
}
]
],
event["receive",
when[
p!=q, (* base guard (s≠r) is strengthened *)
{
r->r+1,
q->1-q 
}
]
]
];

validateModel[myModel3]

Model - digital circuit: pulser

This example is based on chapter 8 of the “Modeling in Event-B” book by Jean-Raymond Abrial.
The model describes a digital circuit that generates one short pulse when a button is pressed.

Initial model

The initial model uses counters to decide when the pulse should be generated, they will disappear in later refinement.

systemMode={env,cir};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel0=model[
axiom["axm0_1",uniqueElements[systemMode]],
invariant["inv0_1",mode∈systemMode],
invariant["inv0_2",{push∈Integers,push≥0}],
invariant["inv0_3",{pop∈Integers,pop≥0}],
invariant["inv0_4",pop≤push],
invariant["inv0_5",push≤pop+1],
invariant["inv0_6",{flash∈Integers,flash≥0}],
invariant["inv0_7",flash≤push],
invariant["inv0_8",push≤flash+1],
invariant["inv0_9",mode==env\[Implies](flash==push||flash==pop)],
(* interesting: without inv0_9, inv0_8 cannot be resolved *)

init["init",{mode->env,push->0,pop->0,flash->0}],

(* events describing abstract environment *)
event["env1",
when[mode==env&&pop==push,
{
mode->cir,
push->push+1
}
]
],
event["env2",
when[mode==env&&pop≠push,
{
mode->cir,
pop->pop+1
}
]
],
event["env3",
when[mode==env,mode->cir]
],

(* events describing abstract circuit *)
event["cir1",
when[mode==cir&&push≠flash,
{
mode->env,
flash->flash+1
}
]
],
event["cir2",
when[mode==cir&&(push≠pop||push==flash),
mode->env
]
]
];

validateModel[myModel0]

First refinement - reducing non-determinism

This refinement reduces non-determinism of the initial model, it follows the first option described in the book (flash the pulse as soon as possible).

myModel1=model[
refines[myModel0],

invariant["inv1_1",(pop≠push&&mode==env)\[Implies]flash≠pop],

event["cir1_pulser"->"cir1", (* in fact, identical to cir1 in base model *)
when[mode==cir&&push≠flash,
{
mode->env,
flash->flash+1
}
]
],
event["cir2_pulser"->"cir2",
when[mode==cir&&push==flash, (* stronger than cir2 *)
mode->env
]
]
];

validateModel[myModel1]

Second refinement - change the data space

This refinement drops the use of integer counters (push, pop, flash) and replaces them with simpler boolean variables (input, output, reg). The challenge is to demonstrate that it is still the same system.

myModel2=model[
refines[myModel1],

invariant["inv2_1",input∈Booleans],
invariant["inv2_2",output∈Booleans],

(* this invariant binds together variables between this and base model, and thus allows to switch data spaces: *)
invariant["inv2_3", (input==True\[Implies]pop≠push)&&(pop≠push\[Implies]input==True)],

invariant["inv2_4",reg∈Booleans], (* single memory register *)
invariant["inv2_5",mode==env\[Implies]reg==input],

invariant["inv2_6",mode==cir\[Implies](
((input==True&&reg==False)\[Implies]push≠flash)&&
(push≠flash\[Implies](input==True&&reg==False))
)],

init["init2",{
input∈Booleans,output∈Booleans,reg∈Booleans,
input->False,output->False,reg->False}],

event["env1",
when[mode==env&&input==False,
{
mode->cir,
input->True
}
]
],
event["env2",
when[mode==env&&input==True,
{
mode->cir,
input->False
}
]
],
event["env3", (* in fact, identical to env3 in base model *)
when[mode==env,mode->cir]
],

event["cir1_pulser",
when[mode==cir&&(input==True&&reg==False),
{
mode->env,
output->True,
reg->input
}
]
],
event["cir2_pulser",
when[mode==cir&&(input==False||reg==True),
{
mode->env,
output->False,
reg->input
}
]
]
];

validateModel[myModel2]

Final circuit

The final refinement merges events that deal with circuit operation (which already use only boolean variables) into a single event that directly defines signal changes as its actions.

myModel3=model[
refines[myModel2],

event["pulser"->{"cir1_pulser","cir2_pulser"},
when[mode==cir,
{
mode->env,

output->((input==True&&reg==False)&&True==True)||
((input==False||reg==True)&&False==True),

reg->(input==True&&(input==True&&reg==False))||
(input==True&&(input==False||reg==True))
}
]
]
];

(* which is the same as: *)
myModel3=model[
refines[myModel2],

event["pulser"->{"cir1_pulser","cir2_pulser"},
when[mode==cir,
{
mode->env,

output->input==True&&reg==False,

reg->input
}
]
]
];

validateModel[myModel3]

Model - digital circuit: arbiter

This example is based on chapter 8 of the “Modeling in Event-B” book by Jean-Raymond Abrial.
The model describes a digital circuit that arbitrates access to resource that is requested by two competing users.

Requirements

reqs=<|
"FUN-1","The circuit has two boolean inputs i_1 and i_2 and two boolean outputs o_1 and o_2.",
"FUN-2","A True input means a user (associated with that input) is asking for a certain resource.",
"FUN-3","The circuit reacts positively to a request by setting the corresponding output to True.",
"FUN-4","The circuit can react positively to only one request at a time (mutual exclusion).",
"FUN-5","Each user frees the resource immediately.",
"FUN-6","A requesting user cannot be postponed indefinitely.",
"FUN-7","A user asking for a resource continues to ask for it as long as it is not served.",
"FUN-8","The resource cannot be granted without a user asking for it."
|>;

Initial model

systemMode={env,cir};

(* helper function for generating statements of unique elements in a set *)
uniqueElements[s_List]:=Unequal@@@Subsets[s,{2}]

myModel0=model[
axiom["axm0_1",uniqueElements[systemMode]],
invariant["inv0_0",mode∈systemMode],

invariant["inv0_1",{r1∈Integers,r1≥0}], (* request counter for user 1 *)
invariant["inv0_2",{r2∈Integers,r2≥0}], (* allocation counter for user 1 *)
invariant["inv0_3",{a1∈Integers,a1≥0}], (* request counter 2 *)
invariant["inv0_4",{a2∈Integers,a2≥0}], (* allocation counter 2 *)

invariant["inv0_5",a1≤r1], (* allocated no more than requested *)
invariant["inv0_6",r1≤a1+1], (* requested until allocated *)
invariant["inv0_7",a2≤r2],
invariant["inv0_8",r2≤a2+1],

invariant["inv0_9",p1∈Booleans], (* p1 is True if user 1 now waits for resource *)
invariant["inv0_10",p2∈Booleans],
invariant["inv0_11",p1==False||p2==False], (* users do not wait together *)

(* glue user actions (r1,a1,r2,a2) with internal knowledge (p1,p2) *)
(*invariant["inv0_12",mode==env\[Implies]((r1==a1\[Implies]p1==False)&&(p1==False\[Implies]r1==a1))],*)
invariant["inv0_12_a",mode==env\[Implies](r1==a1\[Implies]p1==False)],
invariant["inv0_12_b",mode==env\[Implies](p1==False\[Implies]r1==a1)],
(*invariant["inv0_13",mode==env\[Implies]((r2==a2\[Implies]p2==False)&&(p2==False\[Implies]r2==a2))],*)
invariant["inv0_13_a",mode==env\[Implies](r2==a2\[Implies]p2==False)],
invariant["inv0_13_b",mode==env\[Implies](p2==False\[Implies]r2==a2)],
invariant["inv0_14",mode==cir\[Implies](r1==a1\[Implies]p1==False)],
invariant["inv0_15",mode==cir\[Implies](r2==a2\[Implies]p2==False)],

init["init0",
{
r1->0,a1->0,
r2->0,a2->0,
p1∈Booleans,p1->False,
p2∈Booleans,p2->False,
mode->env
}
],

(* environment perspective: user 1 can ask for resource *)
event["env1",
when[mode==env&&r1==a1,
{
mode->cir,
r1->r1+1
}
]
],

(* environment perspective: user 2 can ask for resource *)
event["env2",
when[mode==env&&r2==a2,
{
mode->cir,
r2->r2+1
}
]
],

(* environment perspective: both user can ask for resource *)
event["env3",
when[mode==env&&r1==a1&&r2==a2,
{
mode->cir,
r1->r1+1,
r2->r2+1
}
]
],

(* environment perspective: nothing happens *)
event["env0",
when[mode==env,
mode->cir
]
],

(* circuit perspective: user 1 is waiting for resource (but user 2 is not) *)
event["cir1",
when[mode==cir&&r1≠a1&&p2==False,
{
mode->env,
a1->a1+1, (* allocate to user 1 *)
p1->False,
p2->r2≠a2 (* mark user 2 as waiting, if needed *)
}
]
],

(* circuit perspective: user 2 is waiting for resource (but user 1 is not) *)
event["cir2",
when[mode==cir&&r2≠a2&&p1==False,
{
mode->env,
a2->a2+1, (* allocate to user 2 *)
p2->False,
p1->r1≠a1 (* mark user 1 as waiting, if needed *)
}
]
],

(* circuit perspective: neither user is waiting *)
event["cir0",
when[mode==cir&&r1==a1&&r2==a2,
{
mode->env,
p1->False,
p2->False
}
]
],

deadlockFree[]
];

validateModel[myModel0]

First refinement

The initial model used integer counters to represent both input actions and to influence outputs. This refinement replaces allocation counters with boolean variables, which brings the model closer to the expected boolean system (it is a data space transformation).

(* helper function for counting boolean values, for proving bool variants *)
boolCount[a_]:=If[a==True,1,0]

myModel1=model[
refines[myModel0],

invariant["inv1_1",{b1∈Integers,b1≥0}], (* "past" allocations for user 1 *)
invariant["inv1_2",o1∈Booleans], (* output 1 *)
invariant["inv1_3",{b2∈Integers,b2≥0}], (* "past" allocations for user 2 *)
invariant["inv1_4",o2∈Booleans], (* output 2 *)

(* in the circuit perspective, counters ai and bi are "in phase" *)
invariant["inv1_5",mode==cir\[Implies]a1==b1],
invariant["inv1_6",mode==cir\[Implies]a2==b2],
(* in the environment perspective, ai and bi are possibly shifted by oi *)
invariant["inv1_7",mode==env\[Implies]a1==b1+boolCount[o1]],
invariant["inv1_8",mode==env\[Implies]a2==b2+boolCount[o2]],

(* theorem to help FindInstance solve satisfiability of superposition in events cir1 and cir2 *)
theorem["th1",(a_!=b_)==(a_!=c_)->(a==b&&a==c)||(a!=b&&a!=c)],

init["init1",
{
b1->0,o1∈Booleans,o1->False,
b2->0,o2∈Booleans,o2->False
}
],

event["env1",
when[mode==env&&r1==b1+boolCount[o1],
{
mode->cir,
r1->r1+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2]
}
]
],
event["env2",
when[mode==env&&r2==b2+boolCount[o2],
{
mode->cir,
r2->r2+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2]
}
]
],
event["env3",
when[mode==env&&r1==b1+boolCount[o1]&&r2==b2+boolCount[o2],
{
mode->cir,
r1->r1+1,
r2->r2+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2]
}
]
],
event["env0", (* this event just maintains the shifted counters *)
when[mode==env,
{
mode->cir,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2]
}
]
],

event["cir1",
when[mode==cir&&r1≠b1&&p2==False,
{
mode->env,
o1->True,
o2->False,
p1->False,
p2->r2≠b2
}
]
],
event["cir2",
when[mode==cir&&r2≠b2&&p1==False,
{
mode->env,
o1->False,
o2->True,
p1->r1≠b1,
p2->False
}
]
],
event["cir0",
when[mode==cir&&r1==b1&&r2==b2,
{
mode->env,
o1->False,
o2->False,
p1->False,
p2->False
}
]
]
];

validateModel[myModel1]

Second refinement

In the first refinement, “circuit” events still accessed “environment” state (r1, r2, b1, b2). This refinement introduces boolean variables i1, i2 representing inputs to break this dependency.

myModel2=model[
refines[myModel1],

invariant["inv2_1",i1∈Booleans], (* input for user 1 *)
invariant["inv2_2",i2∈Booleans], (* input for user 2 *)

(* glue *)
(*invariant["inv2_3",mode==cir\[Implies]((i1==False\[Implies]r1==b1)&&(r1==b1\[Implies]i1==False))],*)
invariant["inv2_3_a",mode==cir\[Implies](i1==False\[Implies]r1==b1)],
invariant["inv2_3_b",mode==cir\[Implies](r1==b1\[Implies]i1==False)],
(*invariant["inv2_4",mode==cir\[Implies]((i2==False\[Implies]r2==b2)&&(r2==b2\[Implies]i2==False))],*)
invariant["inv2_4_a",mode==cir\[Implies](i2==False\[Implies]r2==b2)],
invariant["inv2_4_b",mode==cir\[Implies](r2==b2\[Implies]i2==False)],

(* theorem to help FindInstance solve satisfiability of superposition in events cir1 and cir2 *)
theorem["th2",a_==b_==c_->(a&&b&&c)||(!a&&!b&&!c)],

init["init2",{i1∈Booleans,i1->False,i2∈Booleans,i2->False}],

event["env1",
when[mode==env&&r1==b1+boolCount[o1],
{
mode->cir,
r1->r1+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2],
i1->True,
i2->(r2≠b2+boolCount[o2])
}
]
],
event["env2",
when[mode==env&&r2==b2+boolCount[o2],
{
mode->cir,
r2->r2+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2],
i1->(r1≠b1+boolCount[o1]),
i2->True
}
]
],
event["env3",
when[mode==env&&r1==b1+boolCount[o1]&&r2==b2+boolCount[o2],
{
mode->cir,
r1->r1+1,
r2->r2+1,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2],
i1->True,
i2->True
}
]
],
event["env0", (* again, just maintain the counters *)
when[mode==env,
{
mode->cir,
b1->b1+boolCount[o1],
b2->b2+boolCount[o2],
i1->(r1≠b1+boolCount[o1]),
i2->(r2≠b2+boolCount[o2])
}
]
],
event["cir1",
when[mode==cir&&i1==True&&p2==False,
{
mode->env,
o1->True,
o2->False,
p1->False,
p2->i2==True
}
]
],
event["cir2",
when[mode==cir&&i2==True&&p1==False,
{
mode->env,
o1->False,
o2->True,
p1->i1==True,
p2->False
}
]
],
event["cir0",
when[mode==cir&&i1==False&&i2==False,
{
mode->env,
o1->False,
o2->False,
p1->False,
p2->False
}
]
]
];

validateModel[myModel2]

Third refinement

This refinement reduces non-determinacy that allowed both inputs to be set to True and thus allowed both circuit events cir1 and cir2 to be enabled. This refinement gives first user the priority in such case.

myModel3=model[
refines[myModel2],

event["cir1",
when[mode==cir&&i1==True&&p2==False,
{
mode->env,
o1->True,
o2->False,
p2->i2==True
}
]
],
event["cir2",
when[mode==cir&&i2==True&&!(i1==True&&p2==False),
{
mode->env,
o1->False,
o2->True,
p2->False
}
]
],
event["cir0",
when[mode==cir&&i1==False&&i2==False,
{
mode->env,
o1->False,
o2->False,
p2->False
}
]
],

deadlockFree[]
];

validateModel[myModel3]

Final refinement

In this refinement, the “arbiter” event merges together all circuit events from previous model defines the final circuit for both outputs and a single memory register p2.

myModel4=model[
refines[myModel3],

(* theorem to help FindInstance solve satisfiability of superposition in event arbiter on refinement via cir1 and cir2;
(theorem th2 from myModel2 still holds and is used here) *)
theorem["th4",a_==b_==c_==d_->(a&&b&&c&&d)||(!a&&!b&&!c&&!d)],

event["arbiter"->{"cir1","cir2","cir0"}, (* refines all circuit events *)
when[mode==cir,
{
mode->env,

o1->i1==True&&p2==False,
o2->i2==True&&!(i1==True&&p2==False),
p2->i1==True&&i2==True&&p2==False
}
]
]
];

(* with default method->Full the invariant inv1_8 takes forever to prove *)
validateModel[myModel4,method->Piecewise]

Model with non-deterministic actions

This example demonstrates how non-deterministic actions can be refined to become deterministic at the final, concrete level.

The model deals with “earning” and “spending” and the relevant modifications of account state.

Initial model

myModel0=model[
invariant["inv1",account≥0], (* account state, no debts *)
init["init",account->0],

(* at high abstraction level, earning increases the account state *)
event["earn",
{
account->newAccount, (* non-deterministic... *)
newAccount>account (* ...but we know that account increases *)
}
],

(* at high abstraction level, spending decreases the account state *)
event["spend",
when[account>0,
{
account->newAccount, (* non-deterministic... *)
0≤newAccount<account (* but we know that account decreases (but no debts) *)
}
]
]
];

validateModel[myModel0,verbose->Total]

First refinement

In this refinement, earning is constrained to “small” amounts only.
This demonstrates strengthening of promises.

myModel1=model[
refines[myModel0],

event["earn-a-bit"->"earn", (* earning a bit is still earning *)
{
account->newAccount, (* still non-deterministic *)
account<newAccount≤account+1000 (* only small amounts allowed *)
}
]
];

validateModel[myModel1]

Final version

The final refinement uses only deterministic actions.
This demonstrates superposition of state over base promises.

myModel2=model[
refines[myModel1],

event["cut-grass"->"earn-a-bit", (* cutting grass earns a bit! *)
account->account+100 (* deterministic, concrete action *)
],

event["buy-chips"->"spend", (* buying chips is spending *)
when[account>=10,
account->account-10 (* deterministic, concrete action *)
]
]
];

validateModel[myModel2]

Model - sequential program - linear search

This example is based on chapter 15 of the "Modeling in Event-B" book by Jean-Raymond Abrial.
The model describes a linear search algorithm (finding an element in array, for example). Originally, the problem referred to the concept of array and array element explicitly, like in:

r∈Span[1,n];
f[[r]]==v;

where r is an array index, f is an array of size n and v is an element to be found.
However, these details are irrelevant for the algorithm itself, so the notion that r is the interesting index value can be expressed with abstract predicate like this:

good[r]

where “good” has no special meaning from the algorithm point of view. This allows to simplify the deduction engine.

Considering the fact that “good” is not itself defined anywhere, it is a ghost predicate.

Initial version

The initial version just provides structure for the algorithm development - the machine has “progress” and “final” events that will be developed in later refinements.

myModel0=model[
axiom["axiom0_1",{n∈Integers,n≥1}], (* array size *)
invariant["inv0_1",{r∈Integers}], (* array index *)

(* "finishing" event to mark the end of algorithm *)
event["final",
when[good[r],
Null
]
],

(* abstract and non-deterministic progress that "somehow" establishes new index value *)
event["progress",
r>0
]
];

(* Note: this model will NOT validate, because there is no reasonable initial value and also "final" guard has no meaning and is therefore not reachable *)
validateModel[myModel0]

Refinement

This refinement makes the progress action more concrete (it moves the index forward) and introduces an invariant that adds meaning to the “good” predicate.

myModel1a=model[
refines[myModel0],

(* algorithm starts at index 1 *)
init["init1",r->1],

(* index is always within array *)
invariant["inv1_1",r∈Span[1,n]],

(* there is no interesting element in the range that was checked so far *)
invariant["inv1_2",
ForAll[x,x∈Span[1,r-1],¬good[x]]
],

(* variant for event "progress" *)
variant["var1",n-r],

(* concrete algorithm step *)
event["progress",
convergent,
when[r<n∧¬good[r],
r->r+1
]
],

(* "not found" termination event *)
event["failed",
!convergent,
when[r==n∧¬good[r],
Null
]
]
];

validateModel[myModel1a]

Alternative Refinement (with guaranteed success)

This refinement offers a different solution with the assumption that the element searched for is guaranteed to exist somewhere in the array. Thanks to this assumption the “failed” event is not needed and the “progress” event is guaranteed to find the right index without falling out of array.
Axiom “axiom1_1” ensures that the element will be found, ultimately, and invariant “inv1_3” keeps that promise along the process.

In order to prove “inv1_1” here, it is useful to note that:

IF:

n∈(Integers)&&r∈(Integers)&&(Subscript[∃, x,x∈(Integers)&&x∈r;;n])good[x]

THEN:

r==n\[Implies]good[r]

In other words:

IF:

n∈(Integers)&&r∈(Integers)&&(Subscript[∃, x,x∈(Integers)&&x∈r;;n])good[x]

THEN:

¬good[r]\[Implies]r≠n

This means that the guard of event “progress” implies that r!=n, but this has to be injected in terms of a theorem hint.

myModel1b=model[
refines[myModel0],

(* this algorithm assumes that the interesting element is somewhere in the array *)
axiom["axiom1_1",
Exists[x,x∈Span[1,n],good[x]]
],

(* algorithm starts at index 1 *)
init["init1",r->1],

(* index is always within array *)
invariant["inv1_1",r∈Span[1,n]],

(* there is no interesting element in the range that was checked so far... *)
invariant["inv1_2",
ForAll[x,x∈Span[1,r-1],¬good[x]]
],

(* ... the interesting element must be in the remaining part *)
invariant["inv1_3",
Exists[x,x∈Span[r,n],good[x]]
],

(* theorem hint for inv1_1, as explained above *)
theorem["th1",¬good[r]\[Implies]r≠n],

(* variant for event "progress" *)
variant["var1",n-r],

(* concrete algorithm step *)
event["progress",
convergent,
when[¬good[r],
r->r+1
]
]
];

validateModel[myModel1b]

Model - sequential program - binary search in sorted array

This example is based on chapter 15 of the "Modeling in Event-B" book by Jean-Raymond Abrial.
The model describes a binary search algorithm (presumably in a sorted array), and uses ghost predicates to hide the concept of array altogether.

Initial version

As in the linear search example, the initial version is the same and just provides structure for the algorithm development.

myModel0=model[
axiom["axiom0_1",{n∈Integers,n≥1}], (* array size *)
invariant["inv0_1",{r∈Integers}], (* array index *)

(* "finishing" event to mark the end of algorithm *)
event["final",
when[good[r],
Null
]
],

(* abstract and non-deterministic progress that "somehow" establishes new index value *)
event["progress",
r>0
]
];

(* Note: this model will NOT validate completely, because there is no initialization and the ghost predicate good[] is not glued with anything else in the model *)
validateModel[myModel0]

First refinement

In the first refinement we assume that the array contains the interesting element and we introduce two index variable p and q, which will denote the array range where the given element can be found.
The events “inc” and “dec” are partial refinements of base event “progress” and they move p and q in such a way that range p..q inevitably converges. The r index is kept in a non-deterministic way anywhere in p..q.

The ghost predicate “below” indicates that the given index is below the interesting value in the sorted array and predicate “above” indicates that the index is above the final one; as in the previous example, predicate “good” means that the element was found.

myModel1=model[
refines[myModel0],

(* the element is somewhere in the array *)
axiom["axiom1_1",
Exists[x,x∈Span[1,n],good[x]]
],

(* index variables p, q, and r are always within array *)
invariant["inv1_1",p∈Span[1,n]],
invariant["inv1_2",q∈Span[1,n]],
invariant["inv1_3",r∈Span[p,q]], (* r is within p..q *)

(* starting values *)
init["init1",{
p->1,
q->n,
r∈Span[1,n] (* non-deterministic, but within inv1_3 *)
}],

(* the given element is always within range denoted by indices p and q *)
invariant["inv1_4",
Exists[x,x∈Span[p,q],good[x]]
],

(* these theorems bind the "below", "above" and "good" concepts *)
theorem["th1_1",
below[r]\[Implies]ForAll[x,x∈Span[1,r],below[x]∧¬good[x]]
],
theorem["th1_2",
above[r]\[Implies]ForAll[x,x∈Span[r,n],above[x]∧¬good[x]]
],

(* variant for both "inc" and "dec" *)
variant["variant1",q-p],

event["inc"->"progress",
convergent,
when[below[r],
{
(* increase the lower border of the search region *)
p->r+1,

(* set r anywhere in the new region: *)
r->newR,
newR∈Span[r+1,q]
}
]
],
event["dec"->"progress",
convergent,
when[above[r],
{
(* decrease the upper border of the search region *)
q->r-1,

(* set r anywhere in the new region: *)
r->newR,
newR∈Span[p,r-1]
}
]
]
];

validateModel[myModel1]

Second refinement

This (final) refinement reduces the non-determinism of actions by assigning concrete “middle” value for new index.

myModel2=model[
refines[myModel1],

init["init2",{r∈Integers,r->(1+n)/2}],

(* Note:
the underlying engine (ver. 13.3) cannot prove that (for event "inc"):
1+r <= 1+r+IntegerPart[(1/2) (-1+q-r)] <= q
and that the middle value is Integer;
we assume that the above can be proven by "other means" and we replace the problem in place by means of theorem: *)
theorem["th2",
1+r+IntegerPart[(1/2) (-1+q-r)]==newR
->
newR∈1+r;;q
],
(* Similarly, for event "dec": *)
theorem["th2_2",
p+IntegerPart[(1/2) (-1-p+r)]==newR
->
newR∈p;;r-1
],

event["inc",
when[below[r],
{
p->r+1,

(* deterministic middle point *)
(*r->IntegerPart[(r+1+q)/2]*)
r->r+1+IntegerPart[(q-r-1)/2]
}
]
],
event["dec",
when[above[r],
{
q->r-1,

(* deterministic middle point *)
(*r->IntegerPart[(p+r-1)/2]*)
r->p+IntegerPart[(r-1-p)/2]
}
]
]
];

validateModel[myModel2]

Model - sequential program - minimum of an array of natural numbers

This example is based on chapter 15 of the "Modeling in Event-B" book by Jean-Raymond Abrial.
The model uses similar techniques to examples above.

Initial model

The initial model introduces only the array size and states that the array surely contains some “minimal” value.

myModel0=model[
axiom["axiom0_1",{n∈Integers,n≥1}], (* array size *)
axiom["axiom0_2",Exists[x,x∈Span[1,n],minimal[x]]]
];

validateModel[myModel0]

First refinement

This refinement introduces an index range p..q, which presumably contains the minimum array value. It also introduces events “inc” and “dec”, which work towards systematic narrowing of this index range. The “minimalOrGreater” predicate indicates that value at the given index is not lower than the minimal of the whole array. The theorem binds together this concept with comparisons of array values.

myModel1=model[
refines[myModel0],

invariant["inv1_1",p∈Span[1,n]],
invariant["inv1_2",q∈Span[1,n]],
invariant["inv1_3",p≤q],
invariant["inv1_4",Exists[x,x∈Span[p,q],minimal[x]]],

init["init1",{p->1,q->n}],

theorem["th1_1",Function[{knowns,question},
{knowns/.array[p]>array[q]->!minimal[p],question}
]
],
theorem["th1_2",Function[{knowns,question},
{knowns/.array[p]≤array[q]->!minimal[q],question}
]
],

(* variant for "inc" and "dec" *)
variant["var1",q-p],

event["inc",
convergent,
when[p<q&&array[p]>array[q],
p->p+1
]
],
event["dec",
convergent,
when[p<q&&array[p]≤array[q],
q->q-1
]
],
event["minimum",
!convergent,
when[minimal[p],
Null
]
]
];

validateModel[myModel1]

Model - sequential program - pattern for systematic array modification

This model demonstrates the way to describe algorithms that “modify an array”, where neither the modification nor array is directly supported by the syntax. Instead, ghost predicates are used in non-deterministic actions (promises) to guide the proofs. The assumption is that the actual model implementation in some imperative programming language will fulfill those promises.

The model sets all array elements to zero. The “isSetToZero” is a ghost predicate.

myModel=model[
axiom["axiom1",{n∈(Integers),n≥1}], (* array size *)

(* 1..i indicates the range of array that was already processed *)
invariant["inv",i∈(Integers)∧ForAll[x,x∈Span[1,i],isSetToZero[x]]],

init["init",i->0],

variant["var",n-i], (* ensures that progress ultimately finishes *)

event["progress",
convergent,
when[i<n,
{
i->i+1,
isSetToZero[i+1] (* non-deterministic promise *)
}
]
],
event["final", (* marks the end of algorithm *)
when[i==n, (* invariant inv guarantess that the whole array "is set to 0" *)
Null
]
]
];

validateModel[myModel]

Model - sequential program - array partitioning

This example is based on chapter 15 of the “Modeling in Event-B” book by Jean-Raymond Abrial.
The model describes partitioning of array into two parts, where one part (from the beginning) contains elements smaller than the given threshold and the rest (to the end) contains larger elements.

The model does not use the notion of array or element modification directly, but hides them behind ghost predicate, like in previous examples.

Initial model

myModel0=model[
axiom["axiom0_1",{n∈(Integers),n≥1}], (* array size *)

(* k is an index indicating partitioning point *)
invariant["inv0_1",k∈(Integers)],

init["init0",k∈(Integers)], (* non-deterministic *)

event["progress",
k∈(Integers) (* non-deterministic promise *)
],

event["final",
when[ForAll[m,m∈Span[1,k],¬isGreater[m]]∧
ForAll[m,m∈Span[k+1,n],isGreater[m]],
Null
]
]
];

validateModel[myModel0]

First refinement

This refinement introduces variable j that divides the portion of array above k into part that was already processed (k+1..j,  where elements are greater than threshold) and part that was not yet processed (j+1..n). As such, there are three ranges that are managed by the model:
- 1..k, where elements are not greater than threshold (see invariant  inv1_5),
- k+1..j, where elements are greater than threshold (see invariant inv1_6),
- j+1..n, which was not yet processed.
Variable j is also a “loop control variable” in the sense that it starts from 0 and walks up to the end of array.

myModel1=model[
refines[myModel0],

invariant["inv1_1",j∈Span[0,n]],
invariant["inv1_2",k∈Span[0,j]],

(* these invariants describe the already processed part of array *)
invariant["inv1_5",ForAll[m,m∈Span[1,k],¬isGreater[m]]],
invariant["inv1_6",ForAll[m,m∈Span[k+1,j],isGreater[m]]],

init["init1",{j->0,k->0}],

variant["var1",n-j], (* variant for all progress sub-events *)

event["progress_1"->"progress",
convergent,
when[j≠n∧isGreater[j+1],
j->j+1
]
],
event["progress_2"->"progress",
convergent,
when[j≠n∧¬isGreater[j+1]∧k==j,
{
k->k+1,
j->j+1
}
]
],
event["progress_3"->"progress",
convergent,
when[j≠n∧¬isGreater[j+1]∧k≠j,
{
k->k+1,
j->j+1,
¬isGreater[k+1]∧isGreater[j+1] (* non-deterministic promise, presumably implemented as swap of elements at k+1 and j+1 *)
}
]
],
event["final",
when[j==n, (* key point, this is properly matched with condition in base model *)
Null
]
]
];

validateModel[myModel1]

Model - sequential program - simple sorting

This example is based on chapter 15 of the “Modeling in Event-B” book by Jean-Raymond Abrial.
The model uses techniques from earlier examples.

Initial model

In this model, isMinimum[a,b,c] is a (ghost) statement that element at index a is the minimal element from the index range range b..c.

myModel0=model[
axiom["axiom0_1",{n∈(Integers),n≥1}], (* array size *)

event["final",
when[ForAll[i,i∈Span[1,n-1],isMinimum[i,i,n]],
Null
]
]
];

validateModel[myModel0]

First refinement

This refinement introduces index k and promises to keep the invariant that all elements in range 1..k-1 are sorted and not greater than elements in remaining (k..n) part. There is also variable l, which is supposed (but not yet implemented at this level) to point to the minimum element in k..n.

myModel1=model[
refines[myModel0],

invariant["inv1_3",k∈Span[1,n]],
invariant["inv1_4",ForAll[i,i∈Span[1,k-1],isMinimum[i,i,n]]],
invariant["inv1_5",l∈(Integers)],

init["init1",{k->1,l∈(Integers)}],

variant["var1",n-k], (* variant for progress *)

event["progress",
convergent,
when[k≠n∧l∈Span[k,n]∧isMinimum[l,k,n],
{
k->k+1,
l∈(Integers), (* still non-deterministic *)
isMinimum[k,k,n] (* non-deterministic, presumably implemented by swapping elements at k and l *)
}
]
],

event["prog", (* prototype for "nested loop" that finds minimum in k..n *)
¬convergent, (* we don't promise convergence yet *)
l∈(Integers)
],

event["final",
when[k==n, (* with inv1_4 this means that the whole array is sorted *)
Null
]
]
];

validateModel[myModel1]

Second refinement

This refinement develops the “nested loop” of event “prog” that finds the minimum element in range k..n. For this, variable j in this range separates the part that was tested from the part that was not yet tested with l maintained so that it is always at the minimum from k..j.
The whole model maintains the following ranges:
- 1..k-1, which is already sorted with elements less than the rest of array,
- k..j, with l pointing to the minimum in this range (and j walking towards to end),
- j+1..n, which is not yet tested in the given run of the inner loop.
The helper (ghost) predicate isSmaller[a,b] is a statement that element at index a is smaller than element at index b. The relation of this predicate with isMinimum is provided in the form of explicit theorems.

myModel2=model[
refines[myModel1],

invariant["inv2_1",j∈Span[k,n]],
invariant["inv2_2",l∈Span[k,j]],
invariant["inv2_3",isMinimum[l,k,j]],

(* a couple of theorems that inductively explain the meaning of isMinimum *)
theorem["th2_1",isMinimum[l_,l_,l_]->True],
theorem["th2_2",
(isMinimum[l,k,j]∧¬isSmaller[j+1,l])\[Implies]isMinimum[l,k,j+1]],
theorem["th2_3",
(isMinimum[l,k,j]∧isSmaller[j+1,l])\[Implies]isMinimum[j+1,k,j+1]],

(* this theorem allows to discharge reachability of isSmaller predicate,
and also cleans up that predicate after it was used in previous theorems *)
theorem["th2_4",_isSmaller->sm==True&&sm∈Booleans],

init["init2",{k->1,l->1,j->1}],

variant["var2",n-j], (* variant for prog1 and prog2 *)

event["progress",
when[k≠n∧
j==n, (* inv2_3 binds this with the guard of base event *)
{
k->k+1,
j->k+1, (* this restarts the inner loop *)
l->k+1,
isMinimum[k,k,n]  (* still non-deterministic *)
}
]
],

event["prog1"->"prog",
convergent,
when[k≠n∧j≠n∧¬isSmaller[j+1,l],
j->j+1
]
],
event["prog2"->"prog",
convergent,
when[k≠n∧j≠n∧isSmaller[j+1,l],
{
j->j+1,
l->j+1
}
]
]
];

validateModel[myModel2]

Model - sequential program - array reversing

This example is based on chapter 15 of the “Modeling in Event-B” book by Jean-Raymond Abrial.
The model uses techniques from earlier examples.

Initial model

In this model, isSwapped[a] is a (ghost) statement that element at index a and its respective pair from the other end of array (that is, at index n-a+1) are already swapped; it allows to isolate the notion of array from the algorithm itself.

myModel0=model[
axiom["axiom0_1",{n∈(Integers),n≥1}], (* array size *)

event["final",
when[ForAll[k,k∈Span[1,n],isSwapped[k]],
Null
]
]
];

validateModel[myModel0]

First refinement

This refinement introduces indices i and j that move from both sides of array towards each other.

The model maintains three ranges within the array:
- 1..i-1, which is already reversed (with regard to j+1..n),
- i..j, which is still unchanged,
- j+1..n, which is already reversed (with regard to 1..i-1).

Since both i and j traverse towards each other, they maintain the condition i + j == n + 1.

myModel1=model[
refines[myModel0],

invariant["inv1_2",i∈Span[1,n]],
invariant["inv1_3",j∈Span[1,n]],
invariant["inv1_4",i+j==n+1],
invariant["inv1_5",i≤j+1],
invariant["inv1_6",ForAll[k,k∈Span[1,i-1],isSwapped[k]]],
invariant["inv1_8",ForAll[k,k∈Span[j+1,n],isSwapped[k]]],

(* this theorem expresses the fact that swapping always affects two elements at the same time *)
theorem["th1_1",isSwapped[i]\[Implies]isSwapped[n-i+1]],

(* this theorem states that middle element can be considered already swapped *)
axiom["th1_2",ForAll[k,k∈(Integers)&&k==i&&k==j,isSwapped[k]]],

init["init1",{i->1,j->n}],

variant["var1",j-i], (* obiously, shrinking of the middle region *)

event["final",
when[j≤i,
Null
]
],

event["progress",
convergent,
when[i<j,
{
isSwapped[i], (* presumably implemented as swap(A[i], A[n-i+1]) *)
i->i+1,
j->j-1
}
]
]
];

validateModel[myModel1]

Model - sequential program - square root

This example is based on chapter 15 of the “Modeling in Event-B” book by Jean-Raymond Abrial.

The goal of this model is, given input number n, to compute r such that:

(r^2)≤n<(((r+1))^2)

Computing this value is achieved without actual computation of squares - the model is used to verify that the alternative method produces correct results.

Initial model

Initial model just states the expectation with regard to the result.

myModel0=model[
axiom["axiom0",n∈(Integers)&&n>0],

invariant["inv0_1",r∈(Integers)],

init["init0",r∈(Integers)],

event["final",
when[(r^2)≤n<(((r+1))^2),
Null
]
]
];

validateModel[myModel0]

First refinement

This refinement introduces a loop (event “progress”) that finds the result upper bound by brute force.

myModel1=model[
refines[myModel0],

invariant["inv1_1",(r^2)≤n],

init["init1",r->0],

variant["var1",n-r],

event["final",
when[n<(((r+1))^2), (* note: inv1_1 implicitly supports guard compatibility *)
Null
]
],

event["progress",
convergent,
when[(((r+1))^2)≤n,
r->r+1
]
]
];

validateModel[myModel1]

Second refinement

This refinement avoids presumably expensive multiplication (square of r+1) at each step by noticing that:

((((r+1)+1))^2)==(((r+1))^2)+(2r+3)∧
2(r+1)+3==(2r+3)+2

Two more variables a and b maintain the crucial values (((r+1))^2) and 2r + 3. The model verifies (by means of refinement) that the result is correct and fulfills the expectations stated in higher models.

myModel2=model[
refines[myModel1],

invariant["inv2_1",a==(((r+1))^2)],
invariant["inv2_2",b==2r+3],

init["init2",{r->0,a->1,b->3}],

event["final",
when[n<a,
Null
]
],

event["progress",
when[a≤n,
{
r->r+1,
a->a+b,
b->b+2
}
]
]
];

validateModel[myModel2]

Model - coffee machine

The coffee machine model demonstrates the use of refinements and convergent events that add details to the “big-picture” concept defined in base mode.

Base model

The “big-picture” view is that the coffee machine has a single button that can be pressed or released and that button causes the machine to do some work that can be finished and where the machine is idle waiting for another request.

coffeeMachineBase=model[
axiom["axm0",requestButton∈Booleans],
axiom["axm1",inProgress∈Booleans],

init["init0",{requestButton->False,inProgress->False}],

event["button-pressed",
when[¬requestButton,
requestButton->True,
inProgress->True (* the machine is doing something *)
]
],

event["button-released",
when[requestButton,
requestButton->False
]
],

event["work-done",
when[inProgress,
inProgress->False (* the work finishes at some point in time *)
]
],

event["idle",
when[¬inProgress,
Null (* the machine just waits for other requests *)
]
],

deadlockFree[]
];

validateModel[coffeeMachineBase,verbose->Total]

Detailed model

The detailed model adds the concept of “making coffee” and specifies that after some number of coffees (10) it will automatically move to the cleaning task.
Here, making coffee and cleaning are conceptually sub-states of general “work in progress” state that was defined in base model in terms of inProgress flag - but formally these states are defined as new events instead of refinements. This means that they should be convergent, to ensure that they do not starve base events.
The convergence of new events is demonstrated with the help of variant that counts coffees and cleanings together.

boolCount[b_]:=If[b==True,1,0]

coffeeMachine=model[
refines[coffeeMachineBase],

axiom["axiom1-1",coffeeCount∈(Integers)],
axiom["axiom1-2",cleaned∈Booleans],

invariant["inv1-1",coffeeCount>=0],

init["init1",{coffeeCount->0,cleaned->False}],

(* this variant limits the coffee making and cleaning activities *)
variant["make-some-coffees-and-clean",11-coffeeCount-boolCount[cleaned]],

event["make-coffee", (* new event *)
convergent,
when[requestButton∧coffeeCount<10,
{
coffeeCount->coffeeCount+1
}
]
],

event["clean", (* new event *)
convergent,
when[coffeeCount==10∧¬cleaned,
{
inProgress->True,
cleaned->True
}
]
],

event["clean-done"->"work-done", (* refining *)
when[inProgress∧cleaned,
{
inProgress->False,
coffeeCount->0,
cleaned->False
}
]
],

deadlockFree[]
];

validateModel[coffeeMachineMaking,verbose->Total]

Your code here

Good luck!