redex models for pdcfa and cfa2 sections. Use lazy non-determinism and store counting.