Example .::. Computing n²

Computing n² using the accurate implementation

The description of the P system
The Maude modules describing the P system
Examples of rewriting
Searching at non-intermediate configurations

Model checking

The description of the P system

We consider the system: Π₂ = (O, μ, w₁, w₂, w₃, (R₁, ρ₁), (R₂, ρ₂), (R₃, ρ₃), 1), with the following components:

O = {a,b,d,e,f}
μ = [₁ [₂ [₃ ]₃ ]₂]₁,
w₁ = λ, R₁ = &empty, ρ₁ = &empty ,
w₂ = λ, R₂ = {b → d, d → de, r₁ : ff → f, r₂ : f → δ}, ρ₂ = {(r₁, r₂)},
w₃ = a f, R₃ = {a → ab, a → b δ, f → ff }, ρ₃ = Ø ,

The initial configuration of the system is given below:

The initial configuration of the P system

No objects are present in regions 1 and 2, hence no rule can be applied in this regions. The only possibility is to start in membrane 3, by using the single copies of objects a and f.

Using the rules a → ab and f → ff in parallel for all occurrences of a and f currently available, after n steps, n ≥ 0, we get n occurrences of b and 2ⁿ occurrences of f. This way we always have only one copy of a. In any moment, we can use the rule a → bδ instead of a → ab. At that moment we get n+1 occurrences of b and 2ⁿ⁺¹ occurrences of f and the membrane 3 is dissolved. This way the region 3 disappears and all the occurrences of objects from region 3 become occurrences of objects present in region 2. The rules of the membrane 3 are lost and now the rules of membrane 2 are active. Due to the priority relation, we have to use the rule ff → f as much as possible. In one step, we pass from bⁿ⁺¹ to d ⁿ⁺¹, while the number of occurrences of f is halved. In the next step, each occurrence of d introduces one occurrence of e, so we get n+1 occurrences of e and n+1 occurences of d. At the same time, the number of occurrences of f is halved again. The priority relation ensures that this step must be iterated n times, each time producing n+1 occurences of e, and then, when only one copy of f will be present, the rule f → δ must be used. The membrane 2 is dissolved, the rules of region 2 are removed and the objects present here become objects of the skin region, which contains no rules. At this moment no further step is possible and so the computation stops.

Therefore, in the end we have (n+1)(n+1) copies of the object e, for some n≥ 0, present in the skin region. Hence this systems generates numbers of the form n², for n≥ 1.

The Maude module describing the P system

The P system has the following Maude specification:

(mod NSQUARE is
  inc PSYSTEM .

  ops r1 r2 : -> Priority .
  ops M1 M2 M3 : -> Label .
  ops a b d f e : -> Obj .

  op init : -> CConfiguration .
  eq init = { < M1 | empty ; < M2 | empty ; < M3 | a f > > > } .

  eq rules(M3) = (a -> a b), (a -> b delta), (f -> f f) .
  eq freeDeltaRules(M3) = (a -> a b), (f -> f f) .
  eq rho(M3) = empty .

  eq rules(M2) = (b -> d), (d -> d e), (r1 : f f -> f), (r2 : f -> delta) .
  eq freeDeltaRules(M2) = (b -> d), (d -> d e), (r1 : f f -> f) .
  eq rho(M2) = (r1 > r2) .

  eq rules(M1) = none .
  eq freeDeltaRules(M1) = none .
  eq rho(M1) = empty .

  eq maxSize = 15 .
endm)

Examples of rewriting

After loading the the modules PCONFIGURATION, PSYSTEM, and NSQUARE, we can use the command rew to see the intermediat configurations obtained after 25 and 45 steps of rewritings:

Maude> (rew [25] init .)
rewrites: 754 in 5ms cpu (5ms real) (125687 rewrites/second)
rewrite in NSQUARE :
  init
result Configuration? :
  {< M1 | green(empty); < M2 | green(empty); < M3 | green(f f)green(a
    b f f)blue(M3,b,false)> > >}

Maude> (rew [45] init .)
rewrites: 1012 in 6ms cpu (7ms real) (144592 rewrites/second)
rewrite in NSQUARE :
  init
result Configuration? :
  {< M1 | green(empty); < M2 | green(empty); < M3 | green(a b f f f f
    f f) blue(M3,b b f,false)> > >}

Searching configurations in the state space

The following command gives the subspace of reachable configurations (containing at most maxSize objects) starting from the initial configuration:

Maude> (search init =>+ C:Configuration .)
rewrites: 229241 in 1824ms cpu (1824ms real) (125630 rewrites/second)
search in NSQUARE : init =>+ C:Configuration .

Solution 1
C:Configuration <- {< M1 | empty ; < M2 | empty ; < M3 | a b f f > > >}

Solution 2
C:Configuration <- {< M1 | empty ; < M2 | b f f > >}

Solution 3
C:Configuration <- {< M1 | empty ; < M2 | d f > >}

Solution 4
C:Configuration <- {< M1 | empty ; < M2 | empty ; < M3 | a b b f f f f > > >}

Solution 5
C:Configuration <- {< M1 | empty ; < M2 | b b f f f f > >}

Solution 6
C:Configuration <- {< M1 | d e >}

Solution 7
C:Configuration <- {< M1 | empty ; < M2 | d d f f > >}

Solution 8
C:Configuration <- {< M1 | empty ; < M2 | empty ; < M3 | a b b b f f f f f f f
    f > > >}

Solution 9
C:Configuration <- {< M1 | empty ; < M2 | b b b f f f f f f f f > >}

Solution 10
C:Configuration <- {< M1 | empty ; < M2 | d d e e f > >}

Solution 11
C:Configuration <- {< M1 | empty ; < M2 | d d d f f f f > >}

Solution 12
C:Configuration <- {< M1 | d d e e e e >}

Solution 13
C:Configuration <- {< M1 | empty ; < M2 | empty ; < M3 | a b b b b f f f f f f
    f f f f f f f f f f > > >}

Solution 14
C:Configuration <- {< M1 | empty ; < M2 | b b b b f f f f f f f f f f f f f f
    f f > >}

Solution 15
C:Configuration <- {< M1 | empty ; < M2 | d d d e e e f f > >}

Solution 16
C:Configuration <- {< M1 | empty ; < M2 | d d d e e e e e e f > >}

Solution 17
C:Configuration <- {< M1 | d d d e e e e e e e e e >}

No more solutions.

However, we are interested only in the halting configurations, especially in the output membranes from the halting configurations. The command below filters the subspace of reachable committed configurations searching only the halting configurations:

Maude> (search init =>+ { < M1 | S:Soup > } .)
rewrites: 228973 in 1656ms cpu (1656ms real) (138206 rewrites/second)
search in NSQUARE : init =>+ {< M1 | S:Soup >}.

Solution 1
S:Soup <- d e

Solution 2
S:Soup <- d d e e e e

Solution 3
S:Soup <- d d d e e e e e e e e e

No more solutions.

Therefore there are only three halting configurations in the subspace considered, and they give the result for the computation of n^2 for n=1,2,3.

Model checking

We want to check that the number of the occurences of e is the square of the number of the occurrences of b for all final states with the size less than or equal to the given value.

Source code

We illustrate the use of LTL model checker by verifying two atomic propositions:

isHalting, satisfied by a configuration if it is a committed configuration, and it consists of the skin as an elementary membrane (it must be an elementary membrane because the skin is the output membrane);
isSquare, satisfied by a configuration if the number of objects e is the square of the number of objects d.

(mod N2-PREDS is
  including NSQUARE .
  including SATISFACTION .
  subsort Configuration? < State .
  ops isHalting isSquare : -> Prop .
  var C : Configuration? .

  ceq C |= isHalting = true
        if { < M1 | S:Soup > } := C .

  ceq C |= isSquare = true
        if #(C, d) * #(C, d) == #(C, e) .
endm)

(mod PROOF is
  including N2-PREDS .
  including MODEL-CHECKER .
  including LTL-SIMPLIFIER .
endm)

Output

We check the temporal formula

[] (isHalting ->
  isSquare)

by giving the following command:

Maude> (red modelCheck(init, [](isHalting -> isSquare)) .)
rewrites: 235072 in 1829ms cpu (1830ms real) (128474 rewrites/second)
reduce in PROOF :
  modelCheck(init,[](isHalting -> isSquare))
result Bool :
  true

A counter-example

If we slightly modify the isSquare atomic proposition:

  ceq C |= isSquare = true
      if #(C, d) * #(C, d) == #(C, e) + 1 .

then we get a counter-example:

Maude> (red modelCheck(init, [](isHalting -> isSquare)) .)
rewrites: 122514 in 1169ms cpu (1169ms real) (104728 rewrites/second)
reduce in PROOF :
  modelCheck(init,[](isHalting -> isSquare))
result ModelCheckResult :
  counterexample({{< M1 | empty ; < M2 | empty ; < M3 | a f > > >},'1}{{blue(<
    M1 | empty ; < M2 | empty ; < M3 | a f > > >)},'3}{{< M1 | blue(M1,empty);
    blue(< M2 | empty ; < M3 | a f > >)>},'7}{{< M1 | green(empty); blue(< M2 |
    empty ; < M3 | a f > >)>},'3}{{< M1 | green(empty); < M2 | blue(M2,r1 r2,
    empty,false); blue(< M3 | a f >)> >},'9'}{{< M1 | green(empty); < M2 |
    green(empty); blue(< M3 | a f >)> >},'4}{{< M1 | green(empty); < M2 |
    green(empty); < M3 | blue(M3,a f,false)> > >},'6'}{{< M1 | green(empty); <
    M2 | green(empty); < M3 | green(a b)blue(M3,f,false)> > >},'6'}{{< M1 |
    green(empty); < M2 | green(empty); < M3 | green(f f)green(a b)blue(M3,(
    empty).Soup,false)> > >},'14}{{< M1 | green(empty); < M2 | green(empty); <
    M3 | green(a b f f)blue(M3,(empty).Soup,false)> > >},'7'}{{< M1 | green(
    empty); < M2 | green(empty); < M3 | green(empty)green(a b f f)> > >},'14}{{
    < M1 | green(empty); < M2 | green(empty); < M3 | green(a b f f)> > >},'11}{
    {< M1 | green(empty); < M2 | green(empty); green(< M3 | a b f f >)> >},
    '13}{{< M1 | green(empty); green(< M2 | empty ; < M3 | a b f f > >)>},'13}{
    {green(< M1 | empty ; < M2 | empty ; < M3 | a b f f > > >)},'2}{{< M1 |
    empty ; < M2 | empty ; < M3 | a b f f > > >},'1}{{blue(< M1 | empty ; < M2
    | empty ; < M3 | a b f f > > >)},'3}{{< M1 | blue(M1,empty); blue(< M2 |
    empty ; < M3 | a b f f > >)>},'7}{{< M1 | green(empty); blue(< M2 | empty ;
    < M3 | a b f f > >)>},'3}{{< M1 | green(empty); < M2 | blue(M2,r1 r2,empty,
    false); blue(< M3 | a b f f >)> >},'9'}{{< M1 | green(empty); < M2 | green(
    empty); blue(< M3 | a b f f >)> >},'4}{{< M1 | green(empty); < M2 | green(
    empty); < M3 | blue(M3,a b f f,false)> > >},'6'}{{< M1 | green(empty); < M2
    | green(empty); < M3 | green(a b)blue(M3,b f f,false)> > >},'6'}{{< M1 |
    green(empty); < M2 | green(empty); < M3 | green(f f)green(a b)blue(M3,b f,
    false)> > >},'14}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(a
    b f f)blue(M3,b f,false)> > >},'6'}{{< M1 | green(empty); < M2 | green(
    empty); < M3 | green(f f)green(a b f f)blue(M3,b,false)> > >},'14}{{< M1 |
    green(empty); < M2 | green(empty); < M3 | green(a b f f f f)blue(M3,b,
    false)> > >},'7'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(
    b)green(a b f f f f)> > >},'14}{{< M1 | green(empty); < M2 | green(empty);
    < M3 | green(a b b f f f f)> > >},'11}{{< M1 | green(empty); < M2 | green(
    empty); green(< M3 | a b b f f f f >)> >},'13}{{< M1 | green(empty); green(
    < M2 | empty ; < M3 | a b b f f f f > >)>},'13}{{green(< M1 | empty ; < M2
    | empty ; < M3 | a b b f f f f > > >)},'2}{{< M1 | empty ; < M2 | empty ; <
    M3 | a b b f f f f > > >},'1}{{blue(< M1 | empty ; < M2 | empty ; < M3 | a
    b b f f f f > > >)},'3}{{< M1 | blue(M1,empty); blue(< M2 | empty ; < M3 |
    a b b f f f f > >)>},'7}{{< M1 | green(empty); blue(< M2 | empty ; < M3 | a
    b b f f f f > >)>},'3}{{< M1 | green(empty); < M2 | blue(M2,r1 r2,empty,
    false); blue(< M3 | a b b f f f f >)> >},'9'}{{< M1 | green(empty); < M2 |
    green(empty); blue(< M3 | a b b f f f f >)> >},'4}{{< M1 | green(empty); <
    M2 | green(empty); < M3 | blue(M3,a b b f f f f,false)> > >},'6'}{{< M1 |
    green(empty); < M2 | green(empty); < M3 | green(b delta)blue(M3,b b f f f
    f,true)> > >},'6'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(
    f f)green(b delta)blue(M3,b b f f f,true)> > >},'14}{{< M1 | green(empty);
    < M2 | green(empty); < M3 | green(b delta f f)blue(M3,b b f f f,true)> >
    >},'6'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(f f)green(b
    delta f f)blue(M3,b b f f,true)> > >},'14}{{< M1 | green(empty); < M2 |
    green(empty); < M3 | green(b delta f f f f)blue(M3,b b f f,true)> > >},
    '6'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(f f)green(b
    delta f f f f)blue(M3,b b f,true)> > >},'14}{{< M1 | green(empty); < M2 |
    green(empty); < M3 | green(b delta f f f f f f)blue(M3,b b f,true)> > >},
    '6'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(f f)green(b
    delta f f f f f f)blue(M3,b b,true)> > >},'14}{{< M1 | green(empty); < M2 |
    green(empty); < M3 | green(b delta f f f f f f f f)blue(M3,b b,true)> > >},
    '7'}{{< M1 | green(empty); < M2 | green(empty); < M3 | green(b b)green(b
    delta f f f f f f f f)> > >},'14}{{< M1 | green(empty); < M2 | green(
    empty); < M3 | green(b b b delta f f f f f f f f)> > >},'11}{{< M1 | green(
    empty); < M2 | green(empty); green(< M3 | b b b delta f f f f f f f f >)>
    >},'23}{{< M1 | green(empty); < M2 | green(b b b f f f f f f f f)> >},'11}{
    {< M1 | green(empty); green(< M2 | b b b f f f f f f f f >)>},'13}{{green(<
    M1 | empty ; < M2 | b b b f f f f f f f f > >)},'2}{{< M1 | empty ; < M2 |
    b b b f f f f f f f f > >},'1}{{blue(< M1 | empty ; < M2 | b b b f f f f f
    f f f > >)},'3}{{< M1 | blue(M1,empty); blue(< M2 | b b b f f f f f f f f
    >)>},'7}{{< M1 | green(empty); blue(< M2 | b b b f f f f f f f f >)>},'4}{{
    < M1 | green(empty); < M2 | blue(M2,r1 r2,b b b f f f f f f f f,false)> >},
    '8'}{{< M1 | green(empty); < M2 | green(d)blue(M2,r1 r2,b b f f f f f f f
    f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(d)green(d)blue(M2,r1
    r2,b f f f f f f f f,false)> >},'14}{{< M1 | green(empty); < M2 | green(d
    d)blue(M2,r1 r2,b f f f f f f f f,false)> >},'8'}{{< M1 | green(empty); <
    M2 | green(d)green(d d)blue(M2,r1 r2,f f f f f f f f,false)> >},'14}{{< M1
    | green(empty); < M2 | green(d d d)blue(M2,r1 r2,f f f f f f f f,false)>
    >},'8'}{{< M1 | green(empty); < M2 | green(f)green(d d d)blue(M2,r1,f f f f
    f f,false)> >},'14}{{< M1 | green(empty); < M2 | green(d d d f)blue(M2,r1,f
    f f f f f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(f)green(d d d
    f)blue(M2,r1,f f f f,false)> >},'14}{{< M1 | green(empty); < M2 | green(d d
    d f f)blue(M2,r1,f f f f,false)> >},'8'}{{< M1 | green(empty); < M2 |
    green(f)green(d d d f f)blue(M2,r1,f f,false)> >},'14}{{< M1 | green(
    empty); < M2 | green(d d d f f f)blue(M2,r1,f f,false)> >},'8'}{{< M1 |
    green(empty); < M2 | green(f)green(d d d f f f)blue(M2,r1,empty,false)> >},
    '14}{{< M1 | green(empty); < M2 | green(d d d f f f f)blue(M2,r1,empty,
    false)> >},'9'}{{< M1 | green(empty); < M2 | green(empty)green(d d d f f f
    f)> >},'14}{{< M1 | green(empty); < M2 | green(d d d f f f f)> >},'11}{{<
    M1 | green(empty); green(< M2 | d d d f f f f >)>},'13}{{green(< M1 | empty
    ; < M2 | d d d f f f f > >)},'2}{{< M1 | empty ; < M2 | d d d f f f f > >},
    '1}{{blue(< M1 | empty ; < M2 | d d d f f f f > >)},'3}{{< M1 | blue(M1,
    empty); blue(< M2 | d d d f f f f >)>},'7}{{< M1 | green(empty); blue(< M2
    | d d d f f f f >)>},'4}{{< M1 | green(empty); < M2 | blue(M2,r1 r2,d d d f
    f f f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(d e)blue(M2,r1 r2,
    d d f f f f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(d e)green(d
    e)blue(M2,r1 r2,d f f f f,false)> >},'14}{{< M1 | green(empty); < M2 |
    green(d d e e)blue(M2,r1 r2,d f f f f,false)> >},'8'}{{< M1 | green(empty);
    < M2 | green(d e)green(d d e e)blue(M2,r1 r2,f f f f,false)> >},'14}{{< M1
    | green(empty); < M2 | green(d d d e e e)blue(M2,r1 r2,f f f f,false)> >},
    '8'}{{< M1 | green(empty); < M2 | green(f)green(d d d e e e)blue(M2,r1,f f,
    false)> >},'14}{{< M1 | green(empty); < M2 | green(d d d e e e f)blue(M2,
    r1,f f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(f)green(d d d e e
    e f)blue(M2,r1,empty,false)> >},'14}{{< M1 | green(empty); < M2 | green(d d
    d e e e f f)blue(M2,r1,empty,false)> >},'9'}{{< M1 | green(empty); < M2 |
    green(empty)green(d d d e e e f f)> >},'14}{{< M1 | green(empty); < M2 |
    green(d d d e e e f f)> >},'11}{{< M1 | green(empty); green(< M2 | d d d e
    e e f f >)>},'13}{{green(< M1 | empty ; < M2 | d d d e e e f f > >)},'2}{{<
    M1 | empty ; < M2 | d d d e e e f f > >},'1}{{blue(< M1 | empty ; < M2 | d
    d d e e e f f > >)},'3}{{< M1 | blue(M1,empty); blue(< M2 | d d d e e e f f
    >)>},'7}{{< M1 | green(empty); blue(< M2 | d d d e e e f f >)>},'4}{{< M1 |
    green(empty); < M2 | blue(M2,r1 r2,d d d e e e f f,false)> >},'8'}{{< M1 |
    green(empty); < M2 | green(d e)blue(M2,r1 r2,d d e e e f f,false)> >},'8'}{
    {< M1 | green(empty); < M2 | green(d e)green(d e)blue(M2,r1 r2,d e e e f f,
    false)> >},'14}{{< M1 | green(empty); < M2 | green(d d e e)blue(M2,r1 r2,d
    e e e f f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(d e)green(d d
    e e)blue(M2,r1 r2,e e e f f,false)> >},'14}{{< M1 | green(empty); < M2 |
    green(d d d e e e)blue(M2,r1 r2,e e e f f,false)> >},'8'}{{< M1 | green(
    empty); < M2 | green(f)green(d d d e e e)blue(M2,r1,e e e,false)> >},'14}{{
    < M1 | green(empty); < M2 | green(d d d e e e f)blue(M2,r1,e e e,false)>
    >},'9'}{{< M1 | green(empty); < M2 | green(e e e)green(d d d e e e f)> >},
    '14}{{< M1 | green(empty); < M2 | green(d d d e e e e e e f)> >},'11}{{< M1
    | green(empty); green(< M2 | d d d e e e e e e f >)>},'13}{{green(< M1 |
    empty ; < M2 | d d d e e e e e e f > >)},'2}{{< M1 | empty ; < M2 | d d d e
    e e e e e f > >},'1}{{blue(< M1 | empty ; < M2 | d d d e e e e e e f > >)},
    '3}{{< M1 | blue(M1,empty); blue(< M2 | d d d e e e e e e f >)>},'7}{{< M1
    | green(empty); blue(< M2 | d d d e e e e e e f >)>},'4}{{< M1 | green(
    empty); < M2 | blue(M2,r1 r2,d d d e e e e e e f,false)> >},'8'}{{< M1 |
    green(empty); < M2 | green(d e)blue(M2,r1 r2,d d e e e e e e f,false)> >},
    '8'}{{< M1 | green(empty); < M2 | green(d e)green(d e)blue(M2,r1 r2,d e e e
    e e e f,false)> >},'14}{{< M1 | green(empty); < M2 | green(d d e e)blue(M2,
    r1 r2,d e e e e e e f,false)> >},'8'}{{< M1 | green(empty); < M2 | green(d
    e)green(d d e e)blue(M2,r1 r2,e e e e e e f,false)> >},'14}{{< M1 | green(
    empty); < M2 | green(d d d e e e)blue(M2,r1 r2,e e e e e e f,false)> >},
    '8'}{{< M1 | green(empty); < M2 | green(delta)green(d d d e e e)blue(M2,r1
    r2,e e e e e e,true)> >},'14}{{< M1 | green(empty); < M2 | green(d d d
    delta e e e)blue(M2,r1 r2,e e e e e e,true)> >},'9'}{{< M1 | green(empty);
    < M2 | green(e e e e e e)green(d d d delta e e e)> >},'14}{{< M1 | green(
    empty); < M2 | green(d d d delta e e e e e e e e e)> >},'11}{{< M1 | green(
    empty); green(< M2 | d d d delta e e e e e e e e e >)>},'23}{{< M1 | green(
    d d d e e e e e e e e e)>},'12}{{green(< M1 | d d d e e e e e e e e e >)},
    '2},{{< M1 | d d d e e e e e e e e e >},'1}{{blue(< M1 | d d d e e e e e e
    e e e >)},'4}{{< M1 | blue(M1,d d d e e e e e e e e e)>},'7}{{< M1 | green(
    d d d e e e e e e e e e)>},'12}{{green(< M1 | d d d e e e e e e e e e >)},
    '2})

Maude>