Package Demo

We illustrate here how to use the package Electrical.m. For a full description of the package functionality, see notebook Electrical.nb. Also, usage messages for the symbols defined in the package are available.
The commands to the CFLP interpreter are given in input cells. these cells can be recognized by the presence of an In[_] prompt to the left side. For executing them, the user must reach with the cursor in the cell area--either by clicking with the mouse on the cell, or with the arrow keys--and press SHIFT-ENTER.

First, we read in the package by issuing the command

The reading command for Electrical.m executes all the Mathematica commands called in the package. The first two message lines

notify the user on the success of establishing MathLink connections between CFLP interpreter and scheduler, and between scheduler and constraint solvers
The subsequent messages refer to the conditional rewrite rules defined for electrical components and electrical connections. For example, the messages:

refer to the conditional rewrite rules (CRRs) that were defined for serial connections: there are two rules defined, the first one with variables S, L, R, and the second one with variables C1,CS,L,L1,R,S, and L1 being an extra variable (i.e. a variable that does not appear in the left hand side of the CRR).

From now on, the CFLP interpreter and the definitions provided in the sample package Electrical.m are accesible to the user. For getting a list of the symbols created in this sample package, we type in

capacitor earth     EInst     elJoin    inductor  junction  LInst     parallel  resistor  RInst     s         serial    sig       source
CInst

All this symbols have attached a usage message, which can me displayed with the command

?symbol

For example,

indicates the syntax of the capacitor predicate for expressing the behavior of an electrical capacitor. (A more detailed description of our model is available in the notebook Electrical.nb)

Remark:
The pallete CFLPsyntax.nb is provided for typing in CFLP expressions.For using it, use the menu option File/Opem... and select the file CFLPsyntax.nb. The pallete contains templates for the language constructs of the interepreter and looks as shown below.

Using the palette is very simple: a click with the mouse on the palette cell containing the needed template will copy the template to the current cursor position in your Mathematica notebook. The user is required to fill in the placeholders (represented as squares), and jumping from a placeholder to the next one is possible by clicking TAB.
□

This command switches off the warning messages printed by Mathematica when the user defines symbols with similar names.

We can now formulate queries about the behavior of elementary components, e.g.:
õ! dependency of the input signal s[V1,I1] on the output signal s[V2,I2] for a (capacitor or resistor) with characteristic C0

õ! dependency of the output signal s[V2,I2] on the input signal s[V1,I1] for a inductor with characteristic L0

õ! dependency of the output signal s[V2,I2] on the output signal s[V1,I1] for a resistor with characteristic R0

Serial connections

Serial connections are expressed by the predicate serial

A system consisting of a serial connection of n components C1,...,Cn

is described by the predicate

serial[S,{C1,C2,...,Cn},SignIn,SignOut]

Queries for serial connections

õ! dependency of the input signal s[V1,I1] on s[V2,I2] for a serial resistor/capacitor/capacitor connection

õ! serial connection of 3 capacitors: dependency of input signal on output signal; capacitor eqiuvalent to a serial connection of 3 capacitors

How does it work

We illustrate on this example how the calculus proceeds. The initial goal of the calculus is

G1 ≡ {serial[S,{RInst[R],CInst[C1],CInst[C2]},s[I0,V0],s[I1,V1]]~~True}

The infernce rule applied to G1 is outermost narrowing

[on] where f[,...,]→r⇐∧"ï∧ is a fresh variuant of a CRR

since serial is a defined function symbol with two conditional rewrite rules:
(R1) serial[S,•,L,R]→True⇐L~~R
(R2) serial[S,,L,R]→True ⇐ (C1[S,L,L1]~~True ∧ serial[S,CS,L1,R]~~True)

First we apply outermost narrowing [on] w.r.t. (R1) and get

G21≡{S≈S$1079,
>>ť,
s[V0,I0]≈L$1079,s[V1,I1]≈R$1079,True~~True,L$1079~~R$1079}

Next we apply the variable elimination rule [vp] for the parameter passing equation S≈S$1079 and obtain, by applying substitution &thgr;={S$1079↦S} (since S is a constructor), the goal

G31≡{>>≈•, s[V0,I0]≈L$1079,s[V1,I1]≈R$1079,True~~True,L$1079~~R$1079}

Next, we apply outermost narrowing wrt (R.2.) and get

G22≡{S≈S$1080,
>>≈,s[V0,I0]≈L$1080,
s[V1,I1]≈R$1080,True~~True,C1$1080[S$1080,L$1080,L1$1080]~~True,
serial[S$1080,CS$1080,L1$1080,R$1080]~~True}

to which we apply [vp] with &thgr;={S$1080↦S} and next the decomposition rule [d] for constructor terms. We get

G32≡{RInst[R]≈C1$1080,
>≈CS$1080,
s[V0,I0]≈L$1080,
s[V1,I1]≈R$1080,
True~~True,
C1$1080[S,L$1080,L1$1080]~~True,
serial[S,CS$1080,L1$1080,R$1080]~~True}

The next four [vp] inference steps reduce G32 w.r.t. substitution &thgr;={C$1080↦RInst[R], CS$1080↦<CInst[C1],>, L$1080↦s[V0,I0], R$1080↦s[V1,I1]} to goal

G42≡{True~~True,
RInst[R][S,s[I0,V0],L1$1080]~~True,
serial[S,>,L1$1080,s[V1,I1]]~~True}

Equation True~~True is eliminated by a [d] inference step. Since RInst[R] is a placeholder for the &lgr;-term

&lgr;[{S$496,L$496,R$496}, resistor[R,S$496,L$496,R$496]],

the next inference step is outermost &bgr;-reduction [onbeta]. We get the goal

G52≡{resistor[R,S,s[V0,I0],L$1080]~~True,
serial[S,>,L1$1080,s[V1,I1]]~~True}

which reduces in an [on] inference step to

G62≡{R≈R$1081,
S≈S$1081,
s[V0,I0]≈s[V0$1081,I0$1081],
L1$1080≈s[V1$1081,I1$1081],
True~~True,
-V0$1081+V1$1081~~I0$1081 * R$1081,
I0$1081~~I1$1081,
serial[S,>,L1$1080,s[I1,V1]]~~True}

After the inference derivation are [vp],[vp],[d],[vp],[d] we get

G72≡{-V0+V1$1081~~I0 * R,
I0$1081~~I1$1081,
serial[S,>,s[V1$1081,I1],s[V1,I1]]~~True}

The first equation has both sides built up by external function symbols (Plus and respectively Times), and therefore we can only aply a [sp] inference step. This will result in putting equation -V0+V1$1081~~I0 * R into the constraint store. Next, apply [v] inference step and get

G82≡{serial[S,>,s[V1$1081,I1],s[V1,I1]]~~True}

for which there are two alternative outermost narrowing inference steps. The first choice of [on] derives the goal
G821≡{S≈S$1082,
>≈ •,
s[V1$1081,I1]≈L$1082,s[V1,I1]≈R$1082,
True~~True,L$1082~~R$1082}

which can not result in a refutation because of the equation >≈ •.
The second choice of [on] derives trhe goal
G822≡{S≈S$1083,
>≈ ,
s[V1$1081,I1]≈L$1083,s[V1,I1]≈R$1083,
True~~True,
CInst[C1][S$1083,L$1083,L1$1083]~~True,
serial[S$1083,,L1$1083,R$1083]~~True
}

The calculus proceeds until no more equation remains in the goal. At that point, the scheduler is invoked to solve the constraints accumulated so far in the constraint store. Finally, the solutions returned by the scheduler are used to complete the partial solution computed by the CFLP interpreter.

Parallel connections

Parallel connections are expressed by the predicate parallel.

A system consisting of a parallel connection resistor/capacitor/capacitor with specified characteristic values

is described by the predicate

parallel[S,{C1,C2,...,Cn},SignIn,SignOut]

Queries for parallel connections

õ! dependency of SigIn on SigOut for a parallel resistor/capacitor/capacitor conmnection

õ! dependency of SigIn on SigOut for a parallel capacitor/capacitor/capacitor conmnection,
and the capacitor equivalent to such a connection

Mixed connections

For expressing electric components that do not consist only of parallel/serial connections, we make use of the predicate junction which expresses junctions of electric signals.

For example, an electric component of the form

is characterized by the the following conjunction of predicates

junction[{SigIn},{SigIn1,SigIn2}]~~True,
c1[S,SigIn1,SigOut1]~~True,
c2[S,SigIn2,SigOut2]~~True,
junction[{SigOut1},{SigIn3,SigIn4}]~~True,
c3[S,SigIn3,SigOut3]~~True,
junction[{SigOut2,SigOut3},{SigIn5}]~~True,
c4[S,SigIn4,SigOut4]~~True,
c5[S,SigIn5,SigOut5]~~True,
junction[{SigOut4,SigOut5},{SigOut}]~~True.

We define predicate Config1[S,{c1,c2,c3,c4,c5},SignIn,SignOut] for such an electric component

Querries for mixed connections

Dependency of output signal on input signal for Config1 instance witht resistors

determine the characteristic value R1 for the following instance of a Config1 configuration:

when the input/output signals s[I1,V1]/s[I2,V1] are known

We end the CFLP session by closing the connections interpreter/scheduler and scheduler/constraint solvers.