<commit_before>
#include "stabilization.hh"

#include "xnsys.hh"

/**
 * Check for weak convergence to the invariant.
 */
  bool
weak_convergence_ck(const Cx::PFmla& xn, const Cx::PFmla& invariant)
{
#if 1
  return xn.pre_reach(invariant).tautology_ck();
#else
  Cx::PFmla span0( invariant );
  while (!span0.tautology_ck()) {
    const Cx::PFmla& span1 = invariant | xn.pre(span0);
    if (span1.equiv_ck(span0))  return false;
    span0 = span1;
  }
  return true;
#endif
}

  bool
weak_convergence_ck(uint* ret_nlayers, const Cx::PFmla& xn, const Cx::PFmla& invariant, const Cx::PFmla& assumed)
{
  uint nlayers = 1;
  Cx::PFmla visit( invariant );
  Cx::PFmla layer( xn.pre(invariant) - visit );
  while (layer.sat_ck()) {
    visit |= layer;
    layer = (xn.pre(layer) - visit) & assumed;
    if (ret_nlayers) {
      nlayers += 1;
      if (*ret_nlayers > 0 && nlayers > *ret_nlayers) {
        *ret_nlayers = nlayers;
        return false;
      }
    }
  }
  if (ret_nlayers)
    *ret_nlayers = nlayers;
  return assumed.subseteq_ck(visit);
}

  bool
weak_convergence_ck(uint* ret_nlayers, const Cx::PFmla& xn, const Cx::PFmla& invariant)
{
  return weak_convergence_ck(ret_nlayers, xn, invariant, Cx::PFmla(true));
}


  bool
shadow_ck(Cx::PFmla* ret_invariant,
          const Xn::Sys& sys,
          const X::Fmla& lo_xn,
          const X::Fmla& hi_xn,
          const X::Fmlae& lo_xfmlae,
          const P::Fmla& lo_scc,
          const bool explain_failure)
{
  const Xn::Net& topo = sys.topology;
  const Xn::InvariantStyle invariant_style = sys.spec->invariant_style;
  const Xn::InvariantScope invariant_scope = sys.spec->invariant_scope;
  const Xn::InvariantBehav invariant_behav = sys.spec->invariant_behav;
  const Cx::PFmla& shadow_invariant = sys.invariant & sys.closed_assume;

  if (invariant_behav == Xn::FutureSilent) {
    if (lo_scc.sat_ck()) {
      if (explain_failure)
        DBog0( "Protocol is not silent." );
      return false;
    }
  }

  if (!sys.shadow_puppet_synthesis_ck() &&
      invariant_scope != Xn::FutureInvariant)
  {
    // Closure.
    if (!lo_xn.img(shadow_invariant).subseteq_ck(shadow_invariant)) {
      return false;
    }
    // Shadow behavior.
    if (invariant_style != Xn::FutureAndClosed) {
      if (!(sys.shadow_pfmla & shadow_invariant).subseteq_ck(hi_xn)) {
        return false;
      }
      if (!(lo_xn & shadow_invariant).subseteq_ck(sys.shadow_pfmla)) {
        return false;
      }
    }
    // Specification said this should be an active protocol.
    if (invariant_behav == Xn::FutureActiveShadow ||
        invariant_style == Xn::FutureAndActiveShadow)
    {
      if (!shadow_invariant.subseteq_ck(hi_xn.pre())) {
        if (explain_failure)
          DBog0( "Deadlock in invariant." );
        return false;
      }
    }

    if (ret_invariant)
      *ret_invariant = shadow_invariant;
    return true;
  }

  const Cx::PFmla& shadow_self =
    shadow_invariant & topo.proj_shadow(topo.identity_xn);
  const Cx::PFmla& shadow_live =
    shadow_invariant & topo.proj_shadow(sys.shadow_pfmla);

  // There shouldn't be non-progress cycles.
  if (topo.probabilistic_ck()) {
    if (lo_xfmlae.probabilistic_livelock_ck(0, shadow_invariant, shadow_live, &lo_xn)) {
      if (explain_failure)
        DBog0( "Non-progress cycle in invariant." );
      return false;
    }
  }
  else if ((lo_xn & shadow_self).cycle_ck(lo_scc & shadow_live.pre())) {
    if (explain_failure)
      DBog0( "Non-progress cycle in invariant." );
    return false;
  }

  // Invariant states with no transitions to them.
  const Cx::PFmla& shadow_beg =
    shadow_invariant - shadow_live.img();
  // Invariant states with no transitions from them.
  const Cx::PFmla& shadow_end =
    shadow_invariant - shadow_live.pre();

  // Over-approximation of invariant.
  Cx::PFmla hi_invariant = shadow_invariant;
  // Over-approximation of protocol which does not change shadow variables.
  Cx::PFmla hi_self = hi_xn & shadow_self;
  // Over-approximation of protocol which does change shadow variables.
  Cx::PFmla hi_live = hi_xn & shadow_live;

  if (invariant_style == Xn::FutureAndSilent) {
    hi_live = false;
  }
  if (invariant_style == Xn::FutureAndActiveShadow) {
    hi_self = false;
  }

  // Trim all states which cannot be in the invariant since we cannot
  // simulate the shadow protocol in those states given the current
  // over-approximated protocol.
  while (true)
  {
    hi_invariant = lo_xn.closure_within(hi_invariant);
    const Cx::PFmla old_invariant = hi_invariant;

    hi_live &= hi_invariant;
    hi_live &= hi_invariant.as_img();
    hi_live -= (shadow_live - topo.proj_img_shadow(hi_live)).pre();

    hi_invariant -= (lo_xn - (hi_self | hi_live)).pre();

    hi_self &= hi_invariant;
    hi_self &= hi_invariant.as_img();

    hi_invariant &= hi_self.img_reach(shadow_beg | hi_live.img());
    hi_invariant &= hi_self.pre_reach(shadow_end | hi_live.pre());

    if (old_invariant.equiv_ck(hi_invariant)) {
      break;
    }
  }

  Claim( (lo_xn & hi_invariant).subseteq_ck(hi_live | hi_self) );

  if (invariant_scope == Xn::FutureInvariant) {
    // Over-approximated protocol must preserve some part of the invariant.
    if (!hi_invariant.sat_ck()) {
      if (explain_failure) {
        DBog0( "Does not preserve any invariant." );
      }
      return false;<commit_msg>Don't enforce full shadow protocol in all states<commit_after>
#include "stabilization.hh"

#include "xnsys.hh"

/**
 * Check for weak convergence to the invariant.
 */
  bool
weak_convergence_ck(const Cx::PFmla& xn, const Cx::PFmla& invariant)
{
#if 1
  return xn.pre_reach(invariant).tautology_ck();
#else
  Cx::PFmla span0( invariant );
  while (!span0.tautology_ck()) {
    const Cx::PFmla& span1 = invariant | xn.pre(span0);
    if (span1.equiv_ck(span0))  return false;
    span0 = span1;
  }
  return true;
#endif
}

  bool
weak_convergence_ck(uint* ret_nlayers, const Cx::PFmla& xn, const Cx::PFmla& invariant, const Cx::PFmla& assumed)
{
  uint nlayers = 1;
  Cx::PFmla visit( invariant );
  Cx::PFmla layer( xn.pre(invariant) - visit );
  while (layer.sat_ck()) {
    visit |= layer;
    layer = (xn.pre(layer) - visit) & assumed;
    if (ret_nlayers) {
      nlayers += 1;
      if (*ret_nlayers > 0 && nlayers > *ret_nlayers) {
        *ret_nlayers = nlayers;
        return false;
      }
    }
  }
  if (ret_nlayers)
    *ret_nlayers = nlayers;
  return assumed.subseteq_ck(visit);
}

  bool
weak_convergence_ck(uint* ret_nlayers, const Cx::PFmla& xn, const Cx::PFmla& invariant)
{
  return weak_convergence_ck(ret_nlayers, xn, invariant, Cx::PFmla(true));
}


  bool
shadow_ck(Cx::PFmla* ret_invariant,
          const Xn::Sys& sys,
          const X::Fmla& lo_xn,
          const X::Fmla& hi_xn,
          const X::Fmlae& lo_xfmlae,
          const P::Fmla& lo_scc,
          const bool explain_failure)
{
  const Xn::Net& topo = sys.topology;
  const Xn::InvariantStyle invariant_style = sys.spec->invariant_style;
  const Xn::InvariantScope invariant_scope = sys.spec->invariant_scope;
  const Xn::InvariantBehav invariant_behav = sys.spec->invariant_behav;
  const Cx::PFmla& shadow_invariant = sys.invariant & sys.closed_assume;

  if (invariant_behav == Xn::FutureSilent) {
    if (lo_scc.sat_ck()) {
      if (explain_failure)
        DBog0( "Protocol is not silent." );
      return false;
    }
  }

  if (!sys.shadow_puppet_synthesis_ck() &&
      invariant_scope != Xn::FutureInvariant)
  {
    // Closure.
    if (!lo_xn.img(shadow_invariant).subseteq_ck(shadow_invariant)) {
      return false;
    }
    // Shadow behavior.
    if (invariant_style != Xn::FutureAndClosed) {
      if (!(sys.shadow_pfmla & shadow_invariant).subseteq_ck(hi_xn)) {
        return false;
      }
      if (!(lo_xn & shadow_invariant).subseteq_ck(sys.shadow_pfmla)) {
        return false;
      }
    }
    // Specification said this should be an active protocol.
    if (invariant_behav == Xn::FutureActiveShadow ||
        invariant_style == Xn::FutureAndActiveShadow)
    {
      if (!shadow_invariant.subseteq_ck(hi_xn.pre())) {
        if (explain_failure)
          DBog0( "Deadlock in invariant." );
        return false;
      }
    }

    if (ret_invariant)
      *ret_invariant = shadow_invariant;
    return true;
  }

  const Cx::PFmla& shadow_self =
    shadow_invariant & topo.proj_shadow(topo.identity_xn);
  const Cx::PFmla& shadow_live =
    shadow_invariant & topo.proj_shadow(sys.shadow_pfmla);

  // There shouldn't be non-progress cycles.
  if (topo.probabilistic_ck()) {
    if (lo_xfmlae.probabilistic_livelock_ck(0, shadow_invariant, shadow_live, &lo_xn)) {
      if (explain_failure)
        DBog0( "Non-progress cycle in invariant." );
      return false;
    }
  }
  else if ((lo_xn & shadow_self).cycle_ck(lo_scc & shadow_live.pre())) {
    if (explain_failure)
      DBog0( "Non-progress cycle in invariant." );
    return false;
  }

  // Invariant states with no transitions to them.
  const Cx::PFmla& shadow_beg =
    shadow_invariant - shadow_live.img();
  // Invariant states with no transitions from them.
  const Cx::PFmla& shadow_end =
    shadow_invariant - shadow_live.pre();

  // Over-approximation of invariant.
  Cx::PFmla hi_invariant = shadow_invariant;
  // Over-approximation of protocol which does not change shadow variables.
  Cx::PFmla hi_self = hi_xn & shadow_self;
  // Over-approximation of protocol which does change shadow variables.
  Cx::PFmla hi_live = hi_xn & shadow_live;

  if (invariant_style == Xn::FutureAndSilent) {
    hi_live = false;
  }
  if (invariant_style == Xn::FutureAndActiveShadow) {
    hi_self = false;
  }

  // Trim all states which cannot be in the invariant since we cannot
  // simulate the shadow protocol in those states given the current
  // over-approximated protocol.
  while (true)
  {
    hi_invariant = lo_xn.closure_within(hi_invariant);
    const Cx::PFmla old_invariant = hi_invariant;

    hi_live &= hi_invariant;
    hi_live &= hi_invariant.as_img();

    if (invariant_scope == Xn::FutureInvariant) {
      // Remove shadow states where the overapproximated protocol
      // cannot hold all transitions of the shadow protocol.
      hi_live -= (shadow_live - topo.proj_shadow(hi_live)).pre();
    }
    else {
      // Remove puppet states where the overapproximated protocol
      // cannot hold all transitions of the shadow protocol.
      hi_live -= (shadow_live - topo.proj_img_shadow(hi_live)).pre();
      // TODO: This should really have a reachability component.
    }

    hi_invariant -= (lo_xn - (hi_self | hi_live)).pre();

    hi_self &= hi_invariant;
    hi_self &= hi_invariant.as_img();

    hi_invariant &= hi_self.img_reach(shadow_beg | hi_live.img());
    hi_invariant &= hi_self.pre_reach(shadow_end | hi_live.pre());

    if (old_invariant.equiv_ck(hi_invariant)) {
      break;
    }
  }

  Claim( (lo_xn & hi_invariant).subseteq_ck(hi_live | hi_self) );

  if (invariant_scope == Xn::FutureInvariant) {
    // Over-approximated protocol must preserve some part of the invariant.
    if (!hi_invariant.sat_ck()) {
      if (explain_failure) {
        DBog0( "Does not preserve any invariant." );
      }
      return false;
{'fraction_non_alphanumeric': 0.118669757489301, 'fraction_numerical': 0.003209700427960057, 'mean_word_length': 3.2121667292527225, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1638805', 'n_tokens_mistral': 4034, 'n_tokens_neox': 3815, 'n_words': 875}