Trace Slicer for Timed Concurrent Constraint Programming

`General Information`

Concurrent Constraint Programming (CCP) [SRP91] is a declarative model for concurrency aimed at specifying reactive systems, i.e. systems that continuously interact with the environment. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. This tool is a companion for the existing debugging techniques. Slicing in our proposal consists of considering partial computations, which show the presence of bugs. Often, the quantity of information in a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors.

See [FGOP16] for further details.

New!Assertion language. Following the methodology in [FO18] a simple yet powerful assertion language is defined. Assertions allow the user to state properties of the system and to stop automatically the computation when the assertion is not verified. The function assertionStore allows to automatically extract the symptoms from the (failed) assertion in order to start the slicing process. See Examples 2 and 3 above for some testings on the assertion mechanism.

`Download`

The code was implemented in Maude and tested in the version 2.7. Take a look on the header of the files for further details and examples:

csystem.maude: a simple constraint system where constraints are tokens.
assertion.maude: a simple assertion language to state properties of the system.
ntcc.maude: syntax and operational semantics of timed CCP.
slicer.maude: definition of the trace slicer
Example 1: ex1_zigzag.maude (Control for a robot).
Example 2: ex2_rithm.maude (Rhythmic pattern).
Example 3 and 4: ex3_bio.maude and ex3_bio.maude (Biochemical systems).

Download

`References`

[Che07]	M. Chemillier: Les Mathématiques Naturelles. Odile Jacob Press. 2007
[CFHGO13]	Davide Chiarugi, Moreno Falaschi, Diana Hermith, Michell Guzmán, Carlos Olarte: Simulating Signalling Pathways With BioWayS. Electr. Notes Theor. Comput. Sci. 293: 17-34 (2013)
[FGOP16]	M. Falaschi, M. Gabbrielli, C. Olarte and C. Palamidessi: Slicing Concurrent Constraint Programs. LOPSTR 2016. (PDF)
[FO18]	M. Falaschi and C. Olarte: {An Assertion language for slicing Constraint Logic Languages, 2018. (PDF)
[dMDF14]	Elisabetta De Maria, Joëlle Despeyroux, Amy P. Felty: A Logical Framework for Systems Biology. FMMB 2014: 136-155
[NPV02]	Mogens Nielsen, Catuscia Palamidessi, Frank D. Valencia: Temporal Concurrent Constraint Programming: Denotation, Logic and Applications. Nord. J. Comput. 9(1): 145-188 (2002)
[SRP91]	Vijay A. Saraswat, Martin C. Rinard, Prakash Panangaden: Semantic Foundations of Concurrent Constraint Programming. POPL 1991: 333-352

For further information contact Carlos Olarte.

`RCX Robot`

In this example we model a simple RCX robot performing a zigzag (see [NPV02]). The model can be found in the file ex1_zigzag.maude:

maude maude ex1_zigzag.maude

First, we compute a trace with 3 time-units:

rew computeTT(0, 3, zigzag, bot) .

{1 / 3 > 
[0 ; zigzag ; bot][1] --> 
[0 ; right ; bot][1] --> 
[0 ; tell(r) || next(left) ; bot][1] --> 
[0 ; * || next(left) ; r][1] --> stop} ==> 
{2 / 3 > 
[0 ; * || left ; bot][2] --> 
[0 ; * || tell(l) || next(right) ; bot][2] --> 
[0 ; * || * || next(right) ; l][1] --> stop} ==> 
{3 / 3 > 
[0 ; * || * || right ; bot][3] --> 
[0 ; * || * || tell(r) || next(left) ; bot][3] --> 
[0 ; * || * || * || next(left) ; r][1] --> stop} ==> STOP

We can check that in even time-units, the constraint r is irrelevant:

rew ComputeSlice(4, zigzag, (r)) .

{1 / 4 > 
[0 ; * ; *][1] --> stop} ==> 
{2 / 4 > 
[0 ; * ; *][1] --> stop} ==> 
{3 / 4 > 
[0 ; * ; *][1] --> stop} ==> 
{4 / 4 > 
[0 ; * ; *][1] --> stop} ==> STOP

while in odd time-units, it is not:

rew ComputeSlice(3, zigzag, (r)) .

{1 / 3 > 
[0 ; zigzag ; *][1] --> 
[0 ; right ; *][1] --> 
[0 ; next(left) ; *][1] --> stop} ==> 
{2 / 3 > 
[0 ; left ; *][2] --> 
[0 ; next(right) ; *][1] --> stop} ==> 
{3 / 3 > 
[0 ; right ; *][3] --> 
[0 ; tell(r) || * ; *][3] --> 
[0 ; * ; r][1] --> stop} ==> STOP

`Multimedia System`

Consider the following process definitions:

where I_1 = {0,3,5,7,9,11,14,16,18,20,22}, I_2={0,3,5,7,9,11} . This process represents a rhythmic pattern where groups of "2"-unit elements separate groups of "3"-unit elements. Such pattern appears in repertoires of Central African Republic music [Che07].
This pattern can be represented in a circle with 24 divisions, where "2" and "3"-unit elements are placed.

The important property is asymmetry, i.e., if one attempts to break the circle into two parts, it is not possible to have two equal parts. To be more precise, the start and stop constraints divide the circle in two halves (see process Start) and it is always the case that the constraint beat does not coincide in a time-unit with the constraint stop.
If we generate the slice for the time-unit 13 with slicing criteria beat, stop we only observe as relevant process Check (since no beat is produced in that time-unit) :

maude ex2_rithm.maude
rew ComputeSlice(13, System, (beat, stop)) .

{1 / 13 > 
[0 ; System ; *][1] --> 
[0 ; Check ; *][13] --> 
[0 ; ! ask(start, next^12(tell(stop))) ; *][13] --> 
[0 ; ask(start, next^12(tell(stop))) || * ; *][13] --> 
[0 ; next^12(tell(stop)) || * ; *][1] --> stop} ==> 
{2 / 13 > 
[0 ; next^11(tell(stop)) || * ; *][1] --> stop} ==> 
{3 / 13 > 
[0 ; next^10(tell(stop)) || * ; *][1] --> stop} ==> 
{4 / 13 > 
[0 ; next^9(tell(stop)) || * ; *][1] --> stop} ==> 
{5 / 13 > 
[0 ; next^8(tell(stop)) || * ; *][1] --> stop} ==> 
{6 / 13 > 
[0 ; next^7(tell(stop)) || * ; *][1] --> stop} ==> 
{7 / 13 > 
[0 ; next^6(tell(stop)) || * ; *][1] --> stop} ==> 
{8 / 13 > 
[0 ; next^5(tell(stop)) || * ; *][1] --> stop} ==> 
{9 / 13 > 
[0 ; next^4(tell(stop)) || * ; *][1] --> stop} ==> 
{10 / 13 > 
[0 ; next^3(tell(stop)) || * ; *][1] --> stop} ==> 
{11 / 13 > 
[0 ; next^2(tell(stop)) || * ; *][1] --> stop} ==> 
{12 / 13 > 
[0 ; next(tell(stop)) || * ; *][1] --> stop} ==> 
{13 / 13 > 
[0 ; tell(stop) || * ; *][13] --> 
[0 ; * ; stop][1] --> stop} ==> STOP

More interesting, assume that we wrongly write a process Check that is not "well synchronized" with the process Beat. For instance, if I_2'={2}, then the start signal does not coincide with a beat. Then, in time-unit 15, we (wrongly) observe both beat and stop. The trace of that program is quite long and difficult to understand. On the contrary, the sliced one is rather simple:

rew computeTT(0, 15, SystemWrong, bot) .
{1 / 15 > 
[0 ; SystemWrong ; bot][1] --> 
[0 ; Beat || StartWrong || Check ; bot][1] --> 
[0 ; tell(beat) || next^3(tell(beat)) || next^5(tell(beat)) || next^7(tell(
    beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^14(tell(beat))
    || next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(beat)) ||
    next^22(tell(beat)) || StartWrong || Check ; bot][1] --> 
[0 ; * || next^3(tell(beat)) || next^5(tell(beat)) || next^7(tell(beat)) ||
    next^9(tell(beat)) || next^11(tell(beat)) || next^14(tell(beat)) ||
    next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(beat)) ||
    next^22(tell(beat)) || StartWrong || Check ; beat][12] --> 
[0 ; * || next^3(tell(beat)) || next^5(tell(beat)) || next^7(tell(beat)) ||
    next^9(tell(beat)) || next^11(tell(beat)) || next^14(tell(beat)) ||
    next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(beat)) ||
    next^22(tell(beat)) || next^2(tell(start)) || Check ; beat][13] --> 
[0 ; * || next^3(tell(beat)) || next^5(tell(beat)) || next^7(tell(beat)) ||
    next^9(tell(beat)) || next^11(tell(beat)) || next^14(tell(beat)) ||
    next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(beat)) ||
    next^22(tell(beat)) || next^2(tell(start)) || ! ask(start, next^12(tell(
    stop))) ; beat][13] --> 
[0 ; * || next^3(tell(beat)) || next^5(tell(beat)) || next^7(tell(beat)) ||
    next^9(tell(beat)) || next^11(tell(beat)) || next^14(tell(beat)) ||
    next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(beat)) ||
    next^22(tell(beat)) || next^2(tell(start)) || ask(start, next^12(tell(
    stop))) || next(! ask(start, next^12(tell(stop)))) ; beat][1] --> stop} ==>
    
{2 / 15 > 
[0 ; * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(beat)) ||
    next^8(tell(beat)) || next^10(tell(beat)) || next^13(tell(beat)) ||
    next^15(tell(beat)) || next^17(tell(beat)) || next^19(tell(beat)) ||
    next^21(tell(beat)) || next(tell(start)) || ! ask(start, next^12(tell(
    stop))) ; bot][13] --> 
[0 ; * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(beat)) ||
    next^8(tell(beat)) || next^10(tell(beat)) || next^13(tell(beat)) ||
    next^15(tell(beat)) || next^17(tell(beat)) || next^19(tell(beat)) ||
    next^21(tell(beat)) || next(tell(start)) || ask(start, next^12(tell(stop)))
    || next(! ask(start, next^12(tell(stop)))) ; bot][1] --> stop} ==> 
{3 / 15 > 
[0 ; * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^12(tell(beat)) || next^14(
    tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(
    beat)) || tell(start) || ! ask(start, next^12(tell(stop))) ; bot][12] --> 
[0 ; * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^12(tell(beat)) || next^14(
    tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(
    beat)) || * || ! ask(start, next^12(tell(stop))) ; start][13] --> 
[0 ; * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^12(tell(beat)) || next^14(
    tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(
    beat)) || * || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; start][13] --> 
[0 ; * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^12(tell(beat)) || next^14(
    tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || next^20(tell(
    beat)) || * || next^12(tell(stop)) || next(! ask(start, next^12(tell(
    stop)))) ; start][1] --> stop} ==> 
{4 / 15 > 
[0 ; * || tell(beat) || next^2(tell(beat)) || next^4(tell(beat)) || next^6(
    tell(beat)) || next^8(tell(beat)) || next^11(tell(beat)) || next^13(tell(
    beat)) || next^15(tell(beat)) || next^17(tell(beat)) || next^19(tell(beat))
    || * || next^11(tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][2]
    --> 
[0 ; * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(beat))
    || next^8(tell(beat)) || next^11(tell(beat)) || next^13(tell(beat)) ||
    next^15(tell(beat)) || next^17(tell(beat)) || next^19(tell(beat)) || * ||
    next^11(tell(stop)) || ! ask(start, next^12(tell(stop))) ; beat][14] --> 
[0 ; * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(beat))
    || next^8(tell(beat)) || next^11(tell(beat)) || next^13(tell(beat)) ||
    next^15(tell(beat)) || next^17(tell(beat)) || next^19(tell(beat)) || * ||
    next^11(tell(stop)) || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; beat][1] --> stop} ==> 
{5 / 15 > 
[0 ; * || * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat)) ||
    next^14(tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || * ||
    next^10(tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][14] --> 
[0 ; * || * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat)) ||
    next^14(tell(beat)) || next^16(tell(beat)) || next^18(tell(beat)) || * ||
    next^10(tell(stop)) || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; bot][1] --> stop} ==> 
{6 / 15 > 
[0 ; * || * || tell(beat) || next^2(tell(beat)) || next^4(tell(beat)) ||
    next^6(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(
    tell(beat)) || next^15(tell(beat)) || next^17(tell(beat)) || * || next^9(
    tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][3] --> 
[0 ; * || * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(
    beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(tell(beat))
    || next^15(tell(beat)) || next^17(tell(beat)) || * || next^9(tell(stop)) ||
    ! ask(start, next^12(tell(stop))) ; beat][14] --> 
[0 ; * || * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^6(tell(
    beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(tell(beat))
    || next^15(tell(beat)) || next^17(tell(beat)) || * || next^9(tell(stop)) ||
    ask(start, next^12(tell(stop))) || next(! ask(start, next^12(tell(stop))))
    ; beat][1] --> stop} ==> 
{7 / 15 > 
[0 ; * || * || * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(
    beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat))
    || next^14(tell(beat)) || next^16(tell(beat)) || * || next^8(tell(stop)) ||
    ! ask(start, next^12(tell(stop))) ; bot][14] --> 
[0 ; * || * || * || next(tell(beat)) || next^3(tell(beat)) || next^5(tell(
    beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat))
    || next^14(tell(beat)) || next^16(tell(beat)) || * || next^8(tell(stop)) ||
    ask(start, next^12(tell(stop))) || next(! ask(start, next^12(tell(stop))))
    ; bot][1] --> stop} ==> 
{8 / 15 > 
[0 ; * || * || * || tell(beat) || next^2(tell(beat)) || next^4(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(
    tell(beat)) || next^15(tell(beat)) || * || next^7(tell(stop)) || ! ask(
    start, next^12(tell(stop))) ; bot][4] --> 
[0 ; * || * || * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^7(
    tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(tell(
    beat)) || next^15(tell(beat)) || * || next^7(tell(stop)) || ! ask(start,
    next^12(tell(stop))) ; beat][14] --> 
[0 ; * || * || * || * || next^2(tell(beat)) || next^4(tell(beat)) || next^7(
    tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(tell(
    beat)) || next^15(tell(beat)) || * || next^7(tell(stop)) || ask(start,
    next^12(tell(stop))) || next(! ask(start, next^12(tell(stop)))) ; beat][1]
    --> stop} ==> 
{9 / 15 > 
[0 ; * || * || * || * || next(tell(beat)) || next^3(tell(beat)) || next^6(tell(
    beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat))
    || next^14(tell(beat)) || * || next^6(tell(stop)) || ! ask(start, next^12(
    tell(stop))) ; bot][14] --> 
[0 ; * || * || * || * || next(tell(beat)) || next^3(tell(beat)) || next^6(tell(
    beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(beat))
    || next^14(tell(beat)) || * || next^6(tell(stop)) || ask(start, next^12(
    tell(stop))) || next(! ask(start, next^12(tell(stop)))) ; bot][1] --> stop}
    ==> 
{10 / 15 > 
[0 ; * || * || * || * || tell(beat) || next^2(tell(beat)) || next^5(tell(beat))
    || next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) ||
    next^13(tell(beat)) || * || next^5(tell(stop)) || ! ask(start, next^12(
    tell(stop))) ; bot][5] --> 
[0 ; * || * || * || * || * || next^2(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(
    tell(beat)) || * || next^5(tell(stop)) || ! ask(start, next^12(tell(stop)))
    ; beat][14] --> 
[0 ; * || * || * || * || * || next^2(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || next^13(
    tell(beat)) || * || next^5(tell(stop)) || ask(start, next^12(tell(stop)))
    || next(! ask(start, next^12(tell(stop)))) ; beat][1] --> stop} ==> 
{11 / 15 > 
[0 ; * || * || * || * || * || next(tell(beat)) || next^4(tell(beat)) || next^6(
    tell(beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(
    beat)) || * || next^4(tell(stop)) || ! ask(start, next^12(tell(stop))) ;
    bot][14] --> 
[0 ; * || * || * || * || * || next(tell(beat)) || next^4(tell(beat)) || next^6(
    tell(beat)) || next^8(tell(beat)) || next^10(tell(beat)) || next^12(tell(
    beat)) || * || next^4(tell(stop)) || ask(start, next^12(tell(stop))) ||
    next(! ask(start, next^12(tell(stop)))) ; bot][1] --> stop} ==> 
{12 / 15 > 
[0 ; * || * || * || * || * || tell(beat) || next^3(tell(beat)) || next^5(tell(
    beat)) || next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat))
    || * || next^3(tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][6]
    --> 
[0 ; * || * || * || * || * || * || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || * ||
    next^3(tell(stop)) || ! ask(start, next^12(tell(stop))) ; beat][14] --> 
[0 ; * || * || * || * || * || * || next^3(tell(beat)) || next^5(tell(beat)) ||
    next^7(tell(beat)) || next^9(tell(beat)) || next^11(tell(beat)) || * ||
    next^3(tell(stop)) || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; beat][1] --> stop} ==> 
{13 / 15 > 
[0 ; * || * || * || * || * || * || next^2(tell(beat)) || next^4(tell(beat)) ||
    next^6(tell(beat)) || next^8(tell(beat)) || next^10(tell(beat)) || * ||
    next^2(tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][14] --> 
[0 ; * || * || * || * || * || * || next^2(tell(beat)) || next^4(tell(beat)) ||
    next^6(tell(beat)) || next^8(tell(beat)) || next^10(tell(beat)) || * ||
    next^2(tell(stop)) || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; bot][1] --> stop} ==> 
{14 / 15 > 
[0 ; * || * || * || * || * || * || next(tell(beat)) || next^3(tell(beat)) ||
    next^5(tell(beat)) || next^7(tell(beat)) || next^9(tell(beat)) || * ||
    next(tell(stop)) || ! ask(start, next^12(tell(stop))) ; bot][14] --> 
[0 ; * || * || * || * || * || * || next(tell(beat)) || next^3(tell(beat)) ||
    next^5(tell(beat)) || next^7(tell(beat)) || next^9(tell(beat)) || * ||
    next(tell(stop)) || ask(start, next^12(tell(stop))) || next(! ask(start,
    next^12(tell(stop)))) ; bot][1] --> stop} ==> 
{15 / 15 > 
[0 ; * || * || * || * || * || * || tell(beat) || next^2(tell(beat)) || next^4(
    tell(beat)) || next^6(tell(beat)) || next^8(tell(beat)) || * || tell(stop)
    || ! ask(start, next^12(tell(stop))) ; bot][7] --> 
[0 ; * || * || * || * || * || * || * || next^2(tell(beat)) || next^4(tell(
    beat)) || next^6(tell(beat)) || next^8(tell(beat)) || * || tell(stop) || !
    ask(start, next^12(tell(stop))) ; beat][13] --> 
[0 ; * || * || * || * || * || * || * || next^2(tell(beat)) || next^4(tell(
    beat)) || next^6(tell(beat)) || next^8(tell(beat)) || * || * || ! ask(
    start, next^12(tell(stop))) ; beat,stop][14] --> 
[0 ; * || * || * || * || * || * || * || next^2(tell(beat)) || next^4(tell(
    beat)) || next^6(tell(beat)) || next^8(tell(beat)) || * || * || ask(start,
    next^12(tell(stop))) || next(! ask(start, next^12(tell(stop)))) ; beat,
    stop][1] --> stop} ==> STOP

rew ComputeSlice(15, SystemWrong, (beat, stop)) .
{1 / 15 > 
[0 ; SystemWrong ; *][1] --> 
[0 ; Beat || Check ; *][1] --> 
[0 ; next^14(tell(beat)) || Check ; *][13] --> 
[0 ; next^14(tell(beat)) || ! ask(start, next^12(tell(stop))) ; *][13] --> 
[0 ; next^14(tell(beat)) || next(! ask(start, next^12(tell(stop)))) ; *][1] --> stop} ==> 
{2 / 15 > 
[0 ; next^13(tell(beat)) || ! ask(start, next^12(tell(stop))) ; *][13] --> 
[0 ; next^13(tell(beat)) || next(! ask(start, next^12(tell(stop)))) ; *][1] --> stop} ==> 
{3 / 15 > 
[0 ; next^12(tell(beat)) || ! ask(start, next^12(tell(stop))) ; *][13] --> 
[0 ; next^12(tell(beat)) || ask(start, next^12(tell(stop))) || * ; *][13] --> 
[0 ; next^12(tell(beat)) || next^12(tell(stop)) || * ; *][1] --> stop} ==> 
{4 / 15 > 
[0 ; next^11(tell(beat)) || next^11(tell(stop)) || * ; *][1] --> stop} ==> 
{5 / 15 > 
[0 ; next^10(tell(beat)) || next^10(tell(stop)) || * ; *][1] --> stop} ==> 
{6 / 15 > 
[0 ; next^9(tell(beat)) || next^9(tell(stop)) || * ; *][1] --> stop} ==> 
{7 / 15 > 
[0 ; next^8(tell(beat)) || next^8(tell(stop)) || * ; *][1] --> stop} ==> 
{8 / 15 > 
[0 ; next^7(tell(beat)) || next^7(tell(stop)) || * ; *][1] --> stop} ==> 
{9 / 15 > 
[0 ; next^6(tell(beat)) || next^6(tell(stop)) || * ; *][1] --> stop} ==> 
{10 / 15 > 
[0 ; next^5(tell(beat)) || next^5(tell(stop)) || * ; *][1] --> stop} ==> 
{11 / 15 > 
[0 ; next^4(tell(beat)) || next^4(tell(stop)) || * ; *][1] --> stop} ==> 
{12 / 15 > 
[0 ; next^3(tell(beat)) || next^3(tell(stop)) || * ; *][1] --> stop} ==> 
{13 / 15 > 
[0 ; next^2(tell(beat)) || next^2(tell(stop)) || * ; *][1] --> stop} ==> 
{14 / 15 > 
[0 ; next(tell(beat)) || next(tell(stop)) || * ; *][1] --> stop} ==> 
{15 / 15 > 
[0 ; tell(beat) || tell(stop) || * ; *][7] --> 
[0 ; tell(stop) || * ; beat][13] --> 
[0 ; * ; beat,stop][1] --> stop} ==> STOP

Something interesting in this trace is that the ask in the Check process is hidden from the time-unit 4 on (since it is not "needed" any more). Moreover, the only tell(beat) process (from Beat definition) displayed is the one that is executed in time-unit 15. From this trace, it is not difficult to note that the Start process begins its execution on time-unit 3. This can tell the user that the process Start begins its execution in a wrong time-unit.

`Assertions`

The relevant property of the system can be stated in the following assertion

pos(stop) imp neg(beat)

In words, if stop can be deduced then beat must not be deduced from the store. The slicer with the assertion mechanism allows for automatically stop the computation and highlight the relevant information


rew ComputeTraceAssertion('RHYTHM, 20, pos(stop) imp neg(beat) ,SystemWrong) .

`Biochemical Systems`

In [CFHGO13] the ntcc calculus has been used for the specification of biochemical systems. Roughly speaking, the system is represented by a set of reactions of the form: A1 + ... + An --> B1 + ... + Bm meaning that the reaction can be fired if the components A1,...,An are present. In that case, they are consumed and the components B1,..., Bm are produced in the next time-unit.
Recall that the current store in ntcc is not automatically transferred to the next time-unit. Then, we need to specify a process that "moves" to the next time-unit the components not used in a reaction.
Let us exemplify this situation with a simple system with two components "a" and "b" and the following reactions: R1: a --> b
R2: b --> a This system can be specified in ntcc as follows:

R1 = ask('a, tell('aCh) || tell('bCh) || next(tell('b))) .
R2 = ask('b, tell('aCh) || tell('bCh) || next(tell('a))) .
Persistence = ask('a, unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) .
Init = tell('a) .
System = ! R1 || ! R2 || ! Persistence || Init .

In this processes, we use the constraint aCh to signal that the fired rule affects the value of "a" in the next time-unit. Hence, if the rule is fired, the Persistence process cannot modify the state of "a" in the next time-unit (see unless process in the definition of Persistence). The process Init specifies that, in the first time-unit, "a" is present.
If we compute the first 5 time-units, we observe that "a" appears in the odd time-units while "b" is added in the even time-units.

maude ex3_bio.maude 
{1 / 5 > 
[0 ; System ; bot][1] --> 
[0 ; ! R1 || ! R2 || ! Persistence || Init ; bot][1] --> 
[0 ; R1 || next(! R1) || ! R2 || ! Persistence || Init ; bot][1] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ! R2
    || ! Persistence || Init ; bot][3] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || R2 ||
    next(! R2) || ! Persistence || Init ; bot][3] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ask(
    'b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || !
    Persistence || Init ; bot][5] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ask(
    'b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) ||
    Persistence || next(! Persistence) || Init ; bot][5] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ask(
    'b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || ask('a,
    unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) || next(!
    Persistence) || Init ; bot][8] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ask(
    'b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || ask('a,
    unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) || next(!
    Persistence) || tell('a) ; bot][8] --> 
[0 ; ask('a, tell('aCh) || tell('bCh) || next(tell('b))) || next(! R1) || ask(
    'b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || ask('a,
    unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) || next(!
    Persistence) || * ; 'a][1] --> 
[0 ; tell('aCh) || tell('bCh) || next(tell('b)) || next(! R1) || ask('b, tell(
    'aCh) || tell('bCh) || next(tell('a))) || next(! R2) || ask('a, unless(
    'aCh, tell('a))) || ask('b, unless('bCh, tell('b))) || next(! Persistence)
    || * ; 'a][1] --> 
[0 ; * || tell('bCh) || next(tell('b)) || next(! R1) || ask('b, tell('aCh) ||
    tell('bCh) || next(tell('a))) || next(! R2) || ask('a, unless('aCh, tell(
    'a))) || ask('b, unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,
    'aCh][2] --> 
[0 ; * || * || next(tell('b)) || next(! R1) || ask('b, tell('aCh) || tell('bCh)
    || next(tell('a))) || next(! R2) || ask('a, unless('aCh, tell('a))) || ask(
    'b, unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,'aCh,'bCh][7]
    --> 
[0 ; * || * || next(tell('b)) || next(! R1) || ask('b, tell('aCh) || tell('bCh)
    || next(tell('a))) || next(! R2) || unless('aCh, tell('a)) || ask('b,
    unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,'aCh,'bCh][7] --> 
[0 ; * || * || next(tell('b)) || next(! R1) || ask('b, tell('aCh) || tell('bCh)
    || next(tell('a))) || next(! R2) || * || ask('b, unless('bCh, tell('b))) ||
    next(! Persistence) || * ; 'a,'aCh,'bCh][1] --> stop} ==> 
{2 / 5 > 
[0 ; * || * || tell('b) || ! R1 || ! R2 || * || ! Persistence || * ; bot][3]
    --> 
[0 ; * || * || * || ! R1 || ! R2 || * || ! Persistence || * ; 'b][4] --> 
[0 ; * || * || * || R1 || next(! R1) || ! R2 || * || ! Persistence || * ; 'b][
    4] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || ! R2 || * || ! Persistence || * ; 'b][6] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || R2 || next(! R2) || * || ! Persistence || * ; 'b][6] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(!
    R2) || * || ! Persistence || * ; 'b][6] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || tell('aCh) || tell('bCh) || next(tell('a)) || next(! R2) || *
    || ! Persistence || * ; 'b][6] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || tell('bCh) || next(tell('a)) || next(! R2) || * || !
    Persistence || * ; 'aCh,'b][7] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || next(tell('a)) || next(! R2) || * || ! Persistence
    || * ; 'aCh,'b,'bCh][11] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || next(tell('a)) || next(! R2) || * || Persistence ||
    next(! Persistence) || * ; 'aCh,'b,'bCh][11] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || next(tell('a)) || next(! R2) || * || ask('a,
    unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) || next(!
    Persistence) || * ; 'aCh,'b,'bCh][12] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || next(tell('a)) || next(! R2) || * || ask('a,
    unless('aCh, tell('a))) || unless('bCh, tell('b)) || next(! Persistence) ||
    * ; 'aCh,'b,'bCh][12] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || next(tell('a)) || next(! R2) || * || ask('a,
    unless('aCh, tell('a))) || * || next(! Persistence) || * ; 'aCh,'b,'bCh][1]
    --> stop} ==> 
{3 / 5 > 
[0 ; * || * || * || ! R1 || * || * || tell('a) || ! R2 || * || * || !
    Persistence || * ; bot][4] --> 
[0 ; * || * || * || R1 || next(! R1) || * || * || tell('a) || ! R2 || * || * ||
    ! Persistence || * ; bot][4] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || tell('a) || ! R2 || * || * || ! Persistence || * ;
    bot][8] --> 
[0 ; * || * || * || ask('a, tell('aCh) || tell('bCh) || next(tell('b))) ||
    next(! R1) || * || * || * || ! R2 || * || * || ! Persistence || * ; 'a][4]
    --> 
[0 ; * || * || * || tell('aCh) || tell('bCh) || next(tell('b)) || next(! R1) ||
    * || * || * || ! R2 || * || * || ! Persistence || * ; 'a][4] --> 
[0 ; * || * || * || * || tell('bCh) || next(tell('b)) || next(! R1) || * || *
    || * || ! R2 || * || * || ! Persistence || * ; 'a,'aCh][5] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * || !
    R2 || * || * || ! Persistence || * ; 'a,'aCh,'bCh][11] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * || R2
    || next(! R2) || * || * || ! Persistence || * ; 'a,'aCh,'bCh][11] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * ||
    ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || * || *
    || ! Persistence || * ; 'a,'aCh,'bCh][15] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * ||
    ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || * || *
    || Persistence || next(! Persistence) || * ; 'a,'aCh,'bCh][15] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * ||
    ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || * || *
    || ask('a, unless('aCh, tell('a))) || ask('b, unless('bCh, tell('b))) ||
    next(! Persistence) || * ; 'a,'aCh,'bCh][15] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * ||
    ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || * || *
    || unless('aCh, tell('a)) || ask('b, unless('bCh, tell('b))) || next(!
    Persistence) || * ; 'a,'aCh,'bCh][15] --> 
[0 ; * || * || * || * || * || next(tell('b)) || next(! R1) || * || * || * ||
    ask('b, tell('aCh) || tell('bCh) || next(tell('a))) || next(! R2) || * || *
    || * || ask('b, unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,
    'aCh,'bCh][1] --> stop} ==> 
{4 / 5 > 
[0 ; * || * || * || * || * || tell('b) || ! R1 || * || * || * || ! R2 || * || *
    || * || ! Persistence || * ; bot][6] --> 
[0 ; * || * || * || * || * || * || ! R1 || * || * || * || ! R2 || * || * || *
    || ! Persistence || * ; 'b][7] --> 
[0 ; * || * || * || * || * || * || R1 || next(! R1) || * || * || * || ! R2 || *
    || * || * || ! Persistence || * ; 'b][7] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || ! R2 || * || * || * || !
    Persistence || * ; 'b][12] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || R2 || next(! R2) || * || * || *
    || ! Persistence || * ; 'b][12] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || ask('b, tell('aCh) || tell('bCh)
    || next(tell('a))) || next(! R2) || * || * || * || ! Persistence || * ;
    'b][12] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || tell('aCh) || tell('bCh) ||
    next(tell('a)) || next(! R2) || * || * || * || ! Persistence || * ; 'b][12]
    --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || tell('bCh) || next(tell(
    'a)) || next(! R2) || * || * || * || ! Persistence || * ; 'aCh,'b][13] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || next(tell('a)) ||
    next(! R2) || * || * || * || ! Persistence || * ; 'aCh,'b,'bCh][19] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || next(tell('a)) ||
    next(! R2) || * || * || * || Persistence || next(! Persistence) || * ;
    'aCh,'b,'bCh][19] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || next(tell('a)) ||
    next(! R2) || * || * || * || ask('a, unless('aCh, tell('a))) || ask('b,
    unless('bCh, tell('b))) || next(! Persistence) || * ; 'aCh,'b,'bCh][20] -->
    
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || next(tell('a)) ||
    next(! R2) || * || * || * || ask('a, unless('aCh, tell('a))) || unless(
    'bCh, tell('b)) || next(! Persistence) || * ; 'aCh,'b,'bCh][20] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || next(tell('a)) ||
    next(! R2) || * || * || * || ask('a, unless('aCh, tell('a))) || * || next(!
    Persistence) || * ; 'aCh,'b,'bCh][1] --> stop} ==> 
{5 / 5 > 
[0 ; * || * || * || * || * || * || ! R1 || * || * || * || * || * || tell('a) ||
    ! R2 || * || * || * || * || ! Persistence || * ; bot][7] --> 
[0 ; * || * || * || * || * || * || R1 || next(! R1) || * || * || * || * || * ||
    tell('a) || ! R2 || * || * || * || * || ! Persistence || * ; bot][7] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || tell('a) || ! R2 || *
    || * || * || * || ! Persistence || * ; bot][14] --> 
[0 ; * || * || * || * || * || * || ask('a, tell('aCh) || tell('bCh) || next(
    tell('b))) || next(! R1) || * || * || * || * || * || * || ! R2 || * || * ||
    * || * || ! Persistence || * ; 'a][7] --> 
[0 ; * || * || * || * || * || * || tell('aCh) || tell('bCh) || next(tell('b))
    || next(! R1) || * || * || * || * || * || * || ! R2 || * || * || * || * ||
    ! Persistence || * ; 'a][7] --> 
[0 ; * || * || * || * || * || * || * || tell('bCh) || next(tell('b)) || next(!
    R1) || * || * || * || * || * || * || ! R2 || * || * || * || * || !
    Persistence || * ; 'a,'aCh][8] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ! R2 || * || * || * || * || ! Persistence || *
    ; 'a,'aCh,'bCh][17] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || R2 || next(! R2) || * || * || * || * || !
    Persistence || * ; 'a,'aCh,'bCh][17] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ask('b, tell('aCh) || tell('bCh) || next(tell(
    'a))) || next(! R2) || * || * || * || * || ! Persistence || * ; 'a,'aCh,
    'bCh][23] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ask('b, tell('aCh) || tell('bCh) || next(tell(
    'a))) || next(! R2) || * || * || * || * || Persistence || next(!
    Persistence) || * ; 'a,'aCh,'bCh][23] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ask('b, tell('aCh) || tell('bCh) || next(tell(
    'a))) || next(! R2) || * || * || * || * || ask('a, unless('aCh, tell('a)))
    || ask('b, unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,'aCh,
    'bCh][23] --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ask('b, tell('aCh) || tell('bCh) || next(tell(
    'a))) || next(! R2) || * || * || * || * || unless('aCh, tell('a)) || ask(
    'b, unless('bCh, tell('b))) || next(! Persistence) || * ; 'a,'aCh,'bCh][23]
    --> 
[0 ; * || * || * || * || * || * || * || * || next(tell('b)) || next(! R1) || *
    || * || * || * || * || * || ask('b, tell('aCh) || tell('bCh) || next(tell(
    'a))) || next(! R2) || * || * || * || * || * || ask('b, unless('bCh, tell(
    'b))) || next(! Persistence) || * ; 'a,'aCh,'bCh][1] --> stop} ==> STOP

Note that the number of processes executed quickly grows due to the recursive definitions. Then, in a simple system with 2 reactions, debugging is certainly difficult!

`P53/Mdm2 DNA-damage Repair Mechanism`

As a more compelling example, considering the P53/Mdm2 DNA-damage repair mechanism (see, e.g., [dMDF14]). The set of reactions is the following:

R1: Dnadam => ~Mdm2 
R2: ~Mdm2 => P53
R3: P53 => Mdm2
R4: Mdm2 => ~P53
R5: P53 => ~Dnadam 
R6: ~Dnadam => Mdm2

In these equation, "~X" means that the component "X" must be absent.
In order to model this system, for each component "X", we consider 3 constraints:

X to represent that "X" is present.
XA to represent that "X" is absent.
XCh to represent that "X" has changed (due to the application of one of the rules).

Here the ntcc model of the system (see ex4_bio.maude):

R1 = ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) .
R2 = ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53))) .
R3 = ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) .
R4 = ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) .
R5 = ask('P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) .
R6 = ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) .
Persistence = ask('Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) ||
	ask('P53, unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) ||
	ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) .
Init = tell('Dnadam) || tell('Mdm2A) || tell('P53A) .
System = ! R1 || ! R2 || ! R3 || ! R4 || ! R5 || ! R6 || ! Persistence || Init .

Once we execute it, we noticed that something was wrong.

rew computeTT(0, 3, System, bot) .
{1 / 3 > 
[0 ; System ; bot][1] --> 
[0 ; ! R1 || ! R2 || ! R3 || ! R4 || ! R5 || ! R6 || ! Persistence || Init ;
    bot][1] --> 
[0 ; R1 || next(! R1) || ! R2 || ! R3 || ! R4 || ! R5 || ! R6 || ! Persistence
    || Init ; bot][1] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ! R2 || ! R3 || ! R4 || ! R5 || ! R6 || ! Persistence || Init
    ; bot][3] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || R2 || next(! R2) || ! R3 || ! R4 || ! R5 || ! R6 || !
    Persistence || Init ; bot][3] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ! R3 || ! R4 || ! R5 || ! R6 || ! Persistence ||
    Init ; bot][5] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || R3 || next(! R3) || ! R4 || ! R5 || ! R6 || !
    Persistence || Init ; bot][5] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ! R4 || ! R5 || ! R6 || ! Persistence ||
    Init ; bot][7] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || R4 || next(! R4) || ! R5 || ! R6 || !
    Persistence || Init ; bot][7] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ! R5 || ! R6 || ! Persistence || Init ;
    bot][9] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || R5 || next(! R5) || ! R6 || !
    Persistence || Init ; bot][9] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ! R6 || ! Persistence ||
    Init ; bot][11] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || R6 || next(! R6) || !
    Persistence || Init ; bot][11] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || !
    Persistence || Init ; bot][13] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) ||
    Persistence || next(! Persistence) || Init ; bot][13] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) ||
    ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell(
    'Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(!
    Persistence) || Init ; bot][20] --> 
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) ||
    ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell(
    'Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(!
    Persistence) || tell('Dnadam) || tell('Mdm2A) || tell('P53A) ; bot][20] -->
    
[0 ; ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A))) ||
    next(! R1) || ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53))) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(
    tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) ||
    ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell(
    'Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(!
    Persistence) || * || tell('Mdm2A) || tell('P53A) ; 'Dnadam][1] --> 
[0 ; tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2A)) || next(! R1) ||
    ask('Mdm2A, tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(!
    R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) ||
    next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell('P53Ch) ||
    next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || ask('Dnadam, unless(
    'DnadamCh, tell('Dnadam))) || ask('DnadamA, unless('DnadamCh, tell(
    'DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) || ask('P53A, unless(
    'P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask(
    'Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || tell(
    'Mdm2A) || tell('P53A) ; 'Dnadam][1] --> 
[0 ; * || tell('Mdm2Ch) || next(tell('Mdm2A)) || next(! R1) || ask('Mdm2A,
    tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || ask(
    'P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(! R3) ||
    ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(!
    R4) || ask('P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA)))
    || next(! R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(
    tell('Mdm2))) || next(! R6) || ask('Dnadam, unless('DnadamCh, tell(
    'Dnadam))) || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53,
    unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) ||
    ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch,
    tell('Mdm2A))) || next(! Persistence) || * || tell('Mdm2A) || tell('P53A) ;
    'Dnadam,'DnadamCh][2] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || ask('Mdm2A, tell('Mdm2ACh)
    || tell('P53Ch) || next(tell('P53))) || next(! R2) || ask('P53, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(! R3) || ask('Mdm2,
    tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask(
    'P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(!
    R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)))
    || next(! R6) || ask('Dnadam, unless('DnadamCh, tell('Dnadam))) || ask(
    'DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch,
    tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2,
    unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A)))
    || next(! Persistence) || * || tell('Mdm2A) || tell('P53A) ; 'Dnadam,
    'DnadamCh,'Mdm2Ch][15] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || ask('Mdm2A, tell('Mdm2ACh)
    || tell('P53Ch) || next(tell('P53))) || next(! R2) || ask('P53, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(! R3) || ask('Mdm2,
    tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask(
    'P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(!
    R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)))
    || next(! R6) || unless('DnadamCh, tell('Dnadam)) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) ||
    ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell(
    'Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(!
    Persistence) || * || tell('Mdm2A) || tell('P53A) ; 'Dnadam,'DnadamCh,
    'Mdm2Ch][15] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || ask('Mdm2A, tell('Mdm2ACh)
    || tell('P53Ch) || next(tell('P53))) || next(! R2) || ask('P53, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(! R3) || ask('Mdm2,
    tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask(
    'P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(!
    R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)))
    || next(! R6) || * || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) ||
    ask('P53, unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell(
    'P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless(
    'Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || tell('Mdm2A) ||
    tell('P53A) ; 'Dnadam,'DnadamCh,'Mdm2Ch][23] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || ask('Mdm2A, tell('Mdm2ACh)
    || tell('P53Ch) || next(tell('P53))) || next(! R2) || ask('P53, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(! R3) || ask('Mdm2,
    tell('Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask(
    'P53, tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(!
    R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)))
    || next(! R6) || * || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) ||
    ask('P53, unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell(
    'P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless(
    'Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || * || tell('P53A) ;
    'Dnadam,'DnadamCh,'Mdm2A,'Mdm2Ch][5] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || tell('Mdm2ACh) || tell(
    'P53Ch) || next(tell('P53)) || next(! R2) || ask('P53, tell('Mdm2ACh) ||
    tell('P53Ch) || next(tell('Mdm2))) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask('P53,
    tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(! R5) ||
    ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) ||
    next(! R6) || * || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask(
    'P53, unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell(
    'P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless(
    'Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || * || tell('P53A) ;
    'Dnadam,'DnadamCh,'Mdm2A,'Mdm2Ch][5] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || tell('P53Ch) || next(
    tell('P53)) || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell(
    'P53Ch) || next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) ||
    tell('P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell(
    'Mdm2A))) || next(! Persistence) || * || * || tell('P53A) ; 'Dnadam,
    'DnadamCh,'Mdm2A,'Mdm2ACh,'Mdm2Ch][6] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell(
    'Mdm2A))) || next(! Persistence) || * || * || tell('P53A) ; 'Dnadam,
    'DnadamCh,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53Ch][22] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || unless('Mdm2Ch, tell('Mdm2A)) ||
    next(! Persistence) || * || * || tell('P53A) ; 'Dnadam,'DnadamCh,'Mdm2A,
    'Mdm2ACh,'Mdm2Ch,'P53Ch][22] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || * || next(! Persistence) || * || *
    || tell('P53A) ; 'Dnadam,'DnadamCh,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53Ch][26] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || * || next(! Persistence) || * || *
    || * ; 'Dnadam,'DnadamCh,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53A,'P53Ch][20] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || unless('P53Ch, tell('P53A)) || ask('Mdm2, unless(
    'Mdm2Ch, tell('Mdm2))) || * || next(! Persistence) || * || * || * ;
    'Dnadam,'DnadamCh,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53A,'P53Ch][20] --> 
[0 ; * || * || next(tell('Mdm2A)) || next(! R1) || * || * || next(tell('P53))
    || next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ask('Mdm2, tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53A))) || next(! R4) || ask('P53, tell('DnadamCh) || tell(
    'P53Ch) || next(tell('DnadamA))) || next(! R5) || ask('DnadamA, tell(
    'DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * ||
    ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask('P53, unless(
    'P53Ch, tell('P53))) || * || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || *
    || next(! Persistence) || * || * || * ; 'Dnadam,'DnadamCh,'Mdm2A,'Mdm2ACh,
    'Mdm2Ch,'P53A,'P53Ch][1] --> stop} ==> 
{2 / 3 > 
[0 ; * || * || tell('Mdm2A) || ! R1 || * || * || tell('P53) || ! R2 || ! R3 ||
    ! R4 || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; bot][
    3] --> 
[0 ; * || * || * || ! R1 || * || * || tell('P53) || ! R2 || ! R3 || ! R4 || !
    R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A][4] --> 
[0 ; * || * || * || R1 || next(! R1) || * || * || tell('P53) || ! R2 || ! R3 ||
    ! R4 || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ;
    'Mdm2A][4] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || tell('P53) || ! R2 || ! R3 || ! R4 ||
    ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A][8]
    --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || ! R2 || ! R3 || ! R4 || ! R5 || !
    R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'P53][9] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || R2 || next(! R2) || ! R3 || ! R4
    || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,
    'P53][9] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || ask('Mdm2A, tell('Mdm2ACh) ||
    tell('P53Ch) || next(tell('P53))) || next(! R2) || ! R3 || ! R4 || ! R5 ||
    ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'P53][9] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || tell('Mdm2ACh) || tell('P53Ch) ||
    next(tell('P53)) || next(! R2) || ! R3 || ! R4 || ! R5 || ! R6 || * || * ||
    * || ! Persistence || * || * || * ; 'Mdm2A,'P53][9] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || tell('P53Ch) || next(tell(
    'P53)) || next(! R2) || ! R3 || ! R4 || ! R5 || ! R6 || * || * || * || !
    Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53][10] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || ! R3 || ! R4 || ! R5 || ! R6 || * || * || * || ! Persistence
    || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,'P53Ch][13] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || R3 || next(! R3) || ! R4 || ! R5 || ! R6 || * || * || * || !
    Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,'P53Ch][13] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell(
    'Mdm2))) || next(! R3) || ! R4 || ! R5 || ! R6 || * || * || * || !
    Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,'P53Ch][13] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2)) || next(!
    R3) || ! R4 || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || *
    ; 'Mdm2A,'Mdm2ACh,'P53,'P53Ch][13] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || tell('P53Ch) || next(tell('Mdm2)) || next(! R3) || ! R4
    || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,
    'Mdm2ACh,'P53,'P53Ch][14] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ! R4 || ! R5 ||
    ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,
    'P53Ch][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || R4 || next(! R4)
    || ! R5 || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,
    'Mdm2ACh,'P53,'P53Ch][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ! R5 || !
    R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,
    'P53Ch][19] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || R5 ||
    next(! R5) || ! R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,
    'Mdm2ACh,'P53,'P53Ch][19] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || ask('P53,
    tell('DnadamCh) || tell('P53Ch) || next(tell('DnadamA))) || next(! R5) || !
    R6 || * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,
    'P53Ch][19] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || tell(
    'DnadamCh) || tell('P53Ch) || next(tell('DnadamA)) || next(! R5) || ! R6 ||
    * || * || * || ! Persistence || * || * || * ; 'Mdm2A,'Mdm2ACh,'P53,'P53Ch][
    19] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || tell(
    'P53Ch) || next(tell('DnadamA)) || next(! R5) || ! R6 || * || * || * || !
    Persistence || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][20] -->
    
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ! R6 || * || * || * || ! Persistence
    || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][23] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || R6 || next(! R6) || * || * || * || !
    Persistence || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][23] -->
    
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * || !
    Persistence || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][28] -->
    
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * ||
    Persistence || next(! Persistence) || * || * || * ; 'DnadamCh,'Mdm2A,
    'Mdm2ACh,'P53,'P53Ch][28] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || ask('P53, unless('P53Ch, tell('P53))) ||
    ask('P53A, unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell(
    'Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(!
    Persistence) || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][30]
    --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || unless('P53Ch, tell('P53)) || ask('P53A,
    unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) ||
    ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || *
    || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,'P53,'P53Ch][30] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || * || ask('P53A, unless('P53Ch, tell('P53A)))
    || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch,
    tell('Mdm2A))) || next(! Persistence) || * || * || * ; 'DnadamCh,'Mdm2A,
    'Mdm2ACh,'P53,'P53Ch][33] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || next(tell('P53)) ||
    next(! R2) || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * ||
    next(tell('DnadamA)) || next(! R5) || ask('DnadamA, tell('DnadamCh) ||
    tell('Mdm2Ch) || next(tell('Mdm2))) || next(! R6) || * || * || * || ask(
    'Dnadam, unless('DnadamCh, tell('Dnadam))) || ask('DnadamA, unless(
    'DnadamCh, tell('DnadamA))) || * || ask('P53A, unless('P53Ch, tell('P53A)))
    || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || unless('Mdm2Ch, tell(
    'Mdm2A)) || next(! Persistence) || * || * || * ; 'DnadamCh,'Mdm2A,'Mdm2ACh,
    'P53,'P53Ch][1] --> stop} ==> 
{3 / 3 > 
[0 ; * || * || * || ! R1 || * || * || * || * || * || tell('P53) || ! R2 || * ||
    * || tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA) || ! R5 || !
    R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ;
    bot][4] --> 
[0 ; * || * || * || R1 || next(! R1) || * || * || * || * || * || tell('P53) ||
    ! R2 || * || * || tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA)
    || ! R5 || ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || *
    || * || * ; bot][4] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || tell('P53) || ! R2 || *
    || * || tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA) || ! R5 ||
    ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ;
    bot][11] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ! R2 || * || * ||
    tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA) || ! R5 || ! R6 ||
    * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'P53][
    12] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || R2 || next(! R2)
    || * || * || tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA) || !
    R5 || ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || * || *
    || * ; 'P53][12] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * ||
    tell('Mdm2) || ! R3 || ! R4 || * || * || tell('DnadamA) || ! R5 || ! R6 ||
    * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'P53][
    16] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || ! R3 || ! R4 || * || * || tell('DnadamA) || ! R5 || ! R6 || * || * || *
    || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,'P53][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || R3 || next(! R3) || ! R4 || * || * || tell('DnadamA) || ! R5 || ! R6 ||
    * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,
    'P53][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || ask('P53, tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2))) || next(!
    R3) || ! R4 || * || * || tell('DnadamA) || ! R5 || ! R6 || * || * || * || *
    || tell('Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,'P53][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || tell('Mdm2ACh) || tell('P53Ch) || next(tell('Mdm2)) || next(! R3) || !
    R4 || * || * || tell('DnadamA) || ! R5 || ! R6 || * || * || * || * || tell(
    'Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,'P53][17] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || tell('P53Ch) || next(tell('Mdm2)) || next(! R3) || ! R4 || * || *
    || tell('DnadamA) || ! R5 || ! R6 || * || * || * || * || tell('Mdm2A) || !
    Persistence || * || * || * ; 'Mdm2,'Mdm2ACh,'P53][18] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || ! R4 || * || * || tell(
    'DnadamA) || ! R5 || ! R6 || * || * || * || * || tell('Mdm2A) || !
    Persistence || * || * || * ; 'Mdm2,'Mdm2ACh,'P53,'P53Ch][21] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || R4 || next(! R4) || * || *
    || tell('DnadamA) || ! R5 || ! R6 || * || * || * || * || tell('Mdm2A) || !
    Persistence || * || * || * ; 'Mdm2,'Mdm2ACh,'P53,'P53Ch][21] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || ask('Mdm2, tell('Mdm2ACh)
    || tell('P53Ch) || next(tell('P53A))) || next(! R4) || * || * || tell(
    'DnadamA) || ! R5 || ! R6 || * || * || * || * || tell('Mdm2A) || !
    Persistence || * || * || * ; 'Mdm2,'Mdm2ACh,'P53,'P53Ch][21] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || tell('Mdm2ACh) || tell(
    'P53Ch) || next(tell('P53A)) || next(! R4) || * || * || tell('DnadamA) || !
    R5 || ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || * || *
    || * ; 'Mdm2,'Mdm2ACh,'P53,'P53Ch][21] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || tell('P53Ch) || next(
    tell('P53A)) || next(! R4) || * || * || tell('DnadamA) || ! R5 || ! R6 || *
    || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,
    'Mdm2ACh,'P53,'P53Ch][22] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || tell('DnadamA) || ! R5 || ! R6 || * || * || * ||
    * || tell('Mdm2A) || ! Persistence || * || * || * ; 'Mdm2,'Mdm2ACh,'P53,
    'P53Ch][27] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || ! R5 || ! R6 || * || * || * || * || tell(
    'Mdm2A) || ! Persistence || * || * || * ; 'DnadamA,'Mdm2,'Mdm2ACh,'P53,
    'P53Ch][28] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || R5 || next(! R5) || ! R6 || * || * || * ||
    * || tell('Mdm2A) || ! Persistence || * || * || * ; 'DnadamA,'Mdm2,
    'Mdm2ACh,'P53,'P53Ch][28] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || ask('P53, tell('DnadamCh) || tell('P53Ch)
    || next(tell('DnadamA))) || next(! R5) || ! R6 || * || * || * || * || tell(
    'Mdm2A) || ! Persistence || * || * || * ; 'DnadamA,'Mdm2,'Mdm2ACh,'P53,
    'P53Ch][28] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || tell('DnadamCh) || tell('P53Ch) || next(
    tell('DnadamA)) || next(! R5) || ! R6 || * || * || * || * || tell('Mdm2A)
    || ! Persistence || * || * || * ; 'DnadamA,'Mdm2,'Mdm2ACh,'P53,'P53Ch][28]
    --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || tell('P53Ch) || next(tell('DnadamA))
    || next(! R5) || ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence
    || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2ACh,'P53,'P53Ch][29] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || ! R6 || * || * || * || * || tell('Mdm2A) || ! Persistence || * || *
    || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2ACh,'P53,'P53Ch][32] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || R6 || next(! R6) || * || * || * || * || tell('Mdm2A) || !
    Persistence || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2ACh,'P53,
    'P53Ch][32] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || ask('DnadamA, tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)))
    || next(! R6) || * || * || * || * || tell('Mdm2A) || ! Persistence || * ||
    * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2ACh,'P53,'P53Ch][32] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || tell('DnadamCh) || tell('Mdm2Ch) || next(tell('Mdm2)) || next(! R6)
    || * || * || * || * || tell('Mdm2A) || ! Persistence || * || * || * ;
    'DnadamA,'DnadamCh,'Mdm2,'Mdm2ACh,'P53,'P53Ch][32] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || * || tell('Mdm2Ch) || next(tell('Mdm2)) || next(! R6) || * || * || *
    || * || tell('Mdm2A) || ! Persistence || * || * || * ; 'DnadamA,'DnadamCh,
    'Mdm2,'Mdm2ACh,'P53,'P53Ch][33] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || * || * || next(tell('Mdm2)) || next(! R6) || * || * || * || * ||
    tell('Mdm2A) || ! Persistence || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,
    'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][40] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || ask('Mdm2A, tell(
    'Mdm2ACh) || tell('P53Ch) || next(tell('P53))) || next(! R2) || * || * || *
    || * || * || next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A))
    || next(! R4) || * || * || * || * || * || next(tell('DnadamA)) || next(!
    R5) || * || * || next(tell('Mdm2)) || next(! R6) || * || * || * || * || *
    || ! Persistence || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,
    'Mdm2Ch,'P53,'P53Ch][12] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || tell('Mdm2ACh) ||
    tell('P53Ch) || next(tell('P53)) || next(! R2) || * || * || * || * || * ||
    next(tell('Mdm2)) || next(! R3) || * || * || next(tell('P53A)) || next(!
    R4) || * || * || * || * || * || next(tell('DnadamA)) || next(! R5) || * ||
    * || next(tell('Mdm2)) || next(! R6) || * || * || * || * || * || !
    Persistence || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,
    'Mdm2Ch,'P53,'P53Ch][12] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || tell('P53Ch)
    || next(tell('P53)) || next(! R2) || * || * || * || * || * || next(tell(
    'Mdm2)) || next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * ||
    * || * || * || * || next(tell('DnadamA)) || next(! R5) || * || * || next(
    tell('Mdm2)) || next(! R6) || * || * || * || * || * || ! Persistence || *
    || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][
    13] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ! Persistence || * || * || * ;
    'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][43] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || Persistence || next(!
    Persistence) || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,
    'Mdm2Ch,'P53,'P53Ch][43] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || ask('DnadamA, unless('DnadamCh, tell('DnadamA))) || ask(
    'P53, unless('P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell(
    'P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless(
    'Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || * || * ; 'DnadamA,
    'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][44] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || unless('DnadamCh, tell('DnadamA)) || ask('P53, unless(
    'P53Ch, tell('P53))) || ask('P53A, unless('P53Ch, tell('P53A))) || ask(
    'Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch, tell(
    'Mdm2A))) || next(! Persistence) || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,
    'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][44] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || ask('P53, unless('P53Ch, tell('P53))) || ask('P53A,
    unless('P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) ||
    ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || *
    || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][45]
    --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || unless('P53Ch, tell('P53)) || ask('P53A, unless(
    'P53Ch, tell('P53A))) || ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask(
    'Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || * || * ||
    * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][45] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || * || ask('P53A, unless('P53Ch, tell('P53A))) ||
    ask('Mdm2, unless('Mdm2Ch, tell('Mdm2))) || ask('Mdm2A, unless('Mdm2Ch,
    tell('Mdm2A))) || next(! Persistence) || * || * || * ; 'DnadamA,'DnadamCh,
    'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][47] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || * || ask('P53A, unless('P53Ch, tell('P53A))) ||
    unless('Mdm2Ch, tell('Mdm2)) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A)))
    || next(! Persistence) || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,
    'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][47] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || * || ask('P53A, unless('P53Ch, tell('P53A))) || *
    || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || next(! Persistence) || *
    || * || * ; 'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][
    48] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || * || ask('P53A, unless('P53Ch, tell('P53A))) || *
    || unless('Mdm2Ch, tell('Mdm2A)) || next(! Persistence) || * || * || * ;
    'DnadamA,'DnadamCh,'Mdm2,'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][48] --> 
[0 ; * || * || * || ask('Dnadam, tell('DnadamCh) || tell('Mdm2Ch) || next(tell(
    'Mdm2A))) || next(! R1) || * || * || * || * || * || * || * || * || next(
    tell('P53)) || next(! R2) || * || * || * || * || * || next(tell('Mdm2)) ||
    next(! R3) || * || * || next(tell('P53A)) || next(! R4) || * || * || * || *
    || * || next(tell('DnadamA)) || next(! R5) || * || * || next(tell('Mdm2))
    || next(! R6) || * || * || * || * || * || ask('Dnadam, unless('DnadamCh,
    tell('Dnadam))) || * || * || ask('P53A, unless('P53Ch, tell('P53A))) || *
    || * || next(! Persistence) || * || * || * ; 'DnadamA,'DnadamCh,'Mdm2,
    'Mdm2A,'Mdm2ACh,'Mdm2Ch,'P53,'P53Ch][1] --> stop} ==> STOP

Note that, in the last store, we have both Mdm2A and Mdm2 which is wrong! (i.e. Mdm2 is both, absent and present). Our first try was to highlight only those components:

rew ComputeSlice(3, System, ('Mdm2, 'Mdm2A)) .
{1 / 3 > 
[0 ; System ; *][1] --> 
[0 ; ! R3 || ! Persistence || * ; *][5] --> 
[0 ; next(! R3) || ! Persistence || * ; *][13] --> 
[0 ; next(! R3) || next(! Persistence) || * ; *][1] --> stop} ==> 
{2 / 3 > 
[0 ; ! R3 || ! Persistence || * ; *][13] --> 
[0 ; R3 || ! Persistence || * ; *][13] --> 
[0 ; ask('P53, next(tell('Mdm2))) || ! Persistence || * ; *][13] --> 
[0 ; next(tell('Mdm2)) || ! Persistence || * ; *][28] --> 
[0 ; next(tell('Mdm2)) || Persistence || * ; *][28] --> 
[0 ; next(tell('Mdm2)) || ask('Mdm2A, unless('Mdm2Ch, tell('Mdm2A))) || * ; *][33] --> 
[0 ; next(tell('Mdm2)) || unless('Mdm2Ch, tell('Mdm2A)) || * ; *][1] --> stop} ==> 
{3 / 3 > 
[0 ; tell('Mdm2) || tell('Mdm2A) || * ; *][16] --> 
[0 ; tell('Mdm2A) || * ; 'Mdm2,*][40] --> 
[0 ; * ; 'Mdm2,'Mdm2A,*][1] --> stop} ==> STOP

This trace is much simpler than the original one. The slicer highlighted the processes Persistence and R3. Note also that in the end of the second time-unit, we have two active processes:

next(tell('Mdm2)) || unless('Mdm2Ch, tell('Mdm2A))

This means that R3 did not add Mdm2Ch as expected. We then found the bug: we wrongly wrote "'Mdm2ACh" instead of "'Mdm2Ch" in process definition R3.

`Concurrent Rules`

Now consider the initial state

Init = tell('Dnadam) || tell('Mdm2) || tell('P53) .

In that case, we also detect that something is wrong:

rew ComputeSlice(2, System, ('Mdm2, 'Mdm2A)) .
{1 / 2 > 
[0 ; System ; *][1] --> 
[0 ; ! R1 || ! R3 || * ; *][1] --> 
[0 ; R1 || ! R3 || * ; *][1] --> 
[0 ; ask('Dnadam, next(tell('Mdm2A))) || ! R3 || * ; *][5] --> 
[0 ; ask('Dnadam, next(tell('Mdm2A))) || R3 || * ; *][5] --> 
[0 ; ask('Dnadam, next(tell('Mdm2A))) || ask('P53, next(tell('Mdm2))) || * ; *][1] --> 
[0 ; next(tell('Mdm2A)) || ask('P53, next(tell('Mdm2))) || * ; *][7] --> 
[0 ; next(tell('Mdm2A)) || next(tell('Mdm2)) || * ; *][1] --> stop} ==> 
{2 / 2 > 
[0 ; tell('Mdm2A) || tell('Mdm2) || * ; *][3] --> 
[0 ; tell('Mdm2) || * ; 'Mdm2A][6] --> 
[0 ; tell('Mdm2) || * ; 'Mdm2A,*][12] --> 
[0 ; * ; 'Mdm2,'Mdm2A,*][1] --> stop} ==> STOP

Note that, again, we get a store entailing that Mdm2 is both present and absent. The sliced trace shows that, in the first time-unit, the rules R1 and R3 where executed concurrently. In this case, we have two options: either we strength the guard of the reactions to guarantee that all of them are mutually exclusive or we use a choice process (instead of parallel composition) to guarantee that only one rule is fired per time-unit.

`Assertions`

The relevant property of the system can be stated in the following assertion

(pos('Mdm2) imp neg('Mdm2A)) and (pos('Mdm2A) imp neg('Mdm2))

In words, the constraint Mdm2A can be deduced if and only if the constraint Mdm2 cannot be deduced. The slicer with the assertion mechanism allows for automatically stop the computation and highlight the relevant information


rew ComputeTraceAssertion('BIO, 20, (pos('Mdm2) imp neg('Mdm2A)) and (pos('Mdm2A) imp neg('Mdm2)) ,SystemWrong) .