// 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 ];