%% LCR circuit running example
%% 2-d system with dynamics:
%% switch open mode:
%% d Vc/dt = 5-Vc-Vl, d Vl/dt = -5 + Vc - Vl
%% Switch closed mode:
%% d Vc/dt = 5 - 3 Vc - Vl; d Vl/dt = -5 + 3 Vc - Vl
%% We get following invariants: R(xinit,yinit,vxinit,vyinit,x,y,vx,vy):
%% open mode:
%% |Vl|, |Vc-5| <= MAX( |Vlinit|, |Vcinit-5| )
%% closed mode:
%% |Vl|, |Vc-5/3| <= MAX( |Vlinit|, |Vcinit-5/3| )
lcr: CONTEXT =
BEGIN
STATES: TYPE = { open, closed };
RangeV( a:REAL, b:REAL ):[REAL->BOOLEAN] =
{z: REAL | (z <= a OR z <= b OR z <= -a OR z <= -b) AND
(-z <= a OR -z <= b OR -z <= -a OR -z <= -b) };
RangeVc( a:REAL, b:REAL, c:REAL ):[REAL->BOOLEAN] =
{z: REAL | (z-c <= a OR z-c <= b OR z-c <= -a OR z-c <= -b) AND
(-z+c <= a OR -z+c <= b OR -z+c <= -a OR -z+c <= -b) };
lcr: MODULE =
BEGIN
OUTPUT Vl, Vc: REAL
OUTPUT flag: STATES
INITIALIZATION
flag = open;
Vl IN {z: REAL | 0 <= z AND z <= 1};
Vc IN {z: REAL | 1 <= z AND z <= 2}
TRANSITION
[
%% Switch open
flag = open
-->
Vl' IN RangeV( Vl, Vc-5 );
Vc' IN RangeVc(Vl,Vc-5,5)
[]
flag = closed
-->
Vl' IN RangeV( Vl, Vc-5/3 );
Vc' IN RangeVc(Vl,Vc-5/3,5/3)
[]
flag = open AND Vc >= 9/2 AND Vc <= 11/2 --> flag' = closed
[]
flag = closed AND Vc >= 1 AND Vc <= 2 --> flag' = open
]
END;
% Properties and sal-inf-bmc results
% False: 2-step counter-example
vcbad: THEOREM
lcr |- G( Vc <= 5 );
% True, can't prove, but no counter-example found for depth 10 and beyond
vl: THEOREM
lcr |- G( -5 <= Vl AND Vl <= 5 );
% False, counter-example of depth 3 found
vlbad: THEOREM
lcr |- G( Vl <= 2 );
% True, k-induction can't prove, no counter-example found for depth 10
vcvl: THEOREM
lcr |- G( -5 <= Vl AND Vl <= 5 AND -10/3 <= Vc AND Vc <= 10 );
% True, proved by k-induction...just 1-induction.
vcvl2: THEOREM
lcr |- G( -4 <= Vl AND Vl <= 4 AND
( (flag=open AND 1 <= Vc AND Vc <= 9) OR
(flag=closed AND -7/3 <= Vc AND Vc <= 17/3)));
END