Datalog

Some questions are rules: “a host serves when it runs a web server and is not drained; a host is drained when a host it depends on is down.” yen.lib.datalog solves ground rules with negation. Each rule is { head; pos; neg; }. You ground the rules with Nix: one set per host.

{ yen, lib, ... }:
let
  inherit (yen.lib) opt is;
in
{
  yen.kinds.fleet = {
    spawns.host = _: yen.host;
    sinks.out.reduce = yen.lib.reduce.merge;
  };
  yen.kinds.host.fields = {
    web = opt lib.types.bool false;
    maintenance = opt lib.types.bool false;
    dependsOn = opt (is lib.isList) [ ];
  };

  yen.fleet.main = { };
  yen.host.db-1 = { };
  yen.host.db-2.maintenance = true;
  yen.host.web-1 = {
    web = true;
    dependsOn = [ yen.host.db-1 ];
  };
  yen.host.web-2 = {
    web = true;
    dependsOn = [ yen.host.db-2 ];
  };
  yen.flake = { out, ... }: out;
}

# Ground rules { head; pos; neg; }, one set per host. You ground them with Nix.
{ yen, lib, ... }:
let
  D = yen.lib.datalog;
  hosts = lib.attrValues yen.host;
  rules =
    lib.concatMap (
      h:
      let
        n = h.name;
      in
      lib.optional h.web { head = "web:${n}"; }
      ++ lib.optional (!h.maintenance) { head = "up:${n}"; }
      ++ [
        {
          head = "serves:${n}";
          pos = [ "web:${n}" ];
          neg = [ "drained:${n}" ];
        }
      ]
      ++ map (d: {
        head = "drained:${n}";
        neg = [ "up:${d.name}" ];
      }) h.dependsOn
    ) hosts
    # a choice: exactly one primary database, and the policy does not say which
    ++ [
      {
        head = "primary:db-1";
        neg = [ "primary:db-2" ];
      }
      {
        head = "primary:db-2";
        neg = [ "primary:db-1" ];
      }
    ];
  model = D.wfs rules;
in
{
  yen.aspects.serving = {
    at = yen.kinds.fleet;
    out.serving = {
      serves = map (lib.removePrefix "serves:") (lib.filter (lib.hasPrefix "serves:") model.true);
      undefined = model.undefined; # well-founded: the choice stays open
      choices = map (m: lib.filter (lib.hasPrefix "primary:") m) (D.stable rules); # stable models: each choice
      whyNot = D.whyNot rules model "serves:web-2";
      proof = D.proof rules model "serves:web-1";
    };
  };
}

{
  choices = [
    [
      "primary:db-1"
    ]
    [
      "primary:db-2"
    ]
  ];
  proof = {
    atom = "serves:web-1";
    neg = [
      "drained:web-1"
    ];
    pos = [
      {
        atom = "web:web-1";
        neg = [ ];
        pos = [ ];
        rule = {
          head = "web:web-1";
        };
      }
    ];
    rule = {
      head = "serves:web-1";
      neg = [
        "drained:web-1"
      ];
      pos = [
        "web:web-1"
      ];
    };
  };
  serves = [
    "web-1"
  ];
  undefined = [
    "primary:db-1"
    "primary:db-2"
  ];
  whyNot = [
    {
      blocking = [
        "drained:web-2"
      ];
      missing = [ ];
      rule = {
        head = "serves:web-2";
        neg = [
          "drained:web-2"
        ];
        pos = [
          "web:web-2"
        ];
      };
      undefinedBody = [ ];
    }
  ];
}

Function	Answer
`wfs rules`	the well-founded model: `{ true; false; undefined; }`. No strata needed.
`stable rules`	every stable model: one per consistent choice
`why rules model atom`	the rules that prove an atom
`proof rules model atom`	a proof tree; a positive cycle shows `cycle = true`
`whyNot rules model atom`	per rule: the `missing` positive atoms and the `blocking` negative ones
`judge rules a notA`	`supported`, `refuted`, `both`, `neither` or `unknown`
`facts atoms`	atoms as rules with no body

web-2 does not serve: its database db-2 is in maintenance, so web-2 is drained. whyNot says so. The primary database is undefined in the well-founded model. The stable models list the two choices.

Contribute Community Sponsor