// marcie command, e.g.
// marcie --net-file=vilar-bnd-ctl.andl --ctl-file=vilar.ctl --const C1=10,C2=10,k=10
// hint: vary the values for the constants;

// CAUTION: A, R are reserved symbols; 
// so the place names of the two proteins A, R need to be changed to _A, _R.

// Forever it holds that gene A is either free or bound to the activator protein.
AG [ [ geneA=1 & geneA_A=0 ] | [ geneA=0 & geneA_A=1 ] ];

// It is forever possible that there are at least k molecules of protein A,
// which involves liveness of r7;
// yields TRUE for any k <=C2; compare also Exercise 7.9 (d).
AG [ EF [ _A >= k ] ];

// It is forever possible that there are at least k molecules of protein R,
// which involves liveness of r15; 
// yields TRUE for any k <=C2; compare also Exercise 7.9 (d).
AG [ EF [ _R >= k ] ];

// It is possible that there are at the same time at least k molecules of 
// the activator and the repressor; 
// yields TRUE for any k <= C2; compare also Exercise 7.9 (d).
EF [ _A >= k & _R >= k ];