Skip to content
SASY Policy Translation and Enforcement Demo

Policy Walkthrough

This page shows the full policy translation from English to enforced Datalog, clause by clause. The 10-clause policy below is a simplified version used by the 9-scenario demo; the full tau2 airline reference lives at tau2-examples/airline/ — see the benchmark for results.

Three Representations

Section titled “Three Representations”
# Airline Booking Policy


## Default behavior
- All actions are authorized by default


## Cancellation policy
- Gold members can cancel any reservation,
  regardless of insurance status
- Silver and regular members can only cancel
  if the reservation has travel insurance
- Deny cancellation if the reservation has
  no insurance and the member is not gold


## Flight modification policy
- Economy reservations can be modified by any member
- Basic economy reservations can only be modified
  by silver or gold members
- Deny flight modifications on basic economy
  reservations for regular members

Clause-by-Clause Breakdown

Section titled “Clause-by-Clause Breakdown”

Each clause maps English intent to a concrete Datalog rule. Click to expand.

C1: Authorize all actions by default

English: “All actions are authorized by default”

Datalog:

IsAuthorized(idx) :- Actions(idx, _).

Every tool call is allowed unless a specific Unauthorized rule overrides it. Without this rule, tools like get_reservation_details would be blocked — even though the policy has no rules about them.

Cancellation Rules

Section titled “Cancellation Rules”
C2: Allow cancel if gold member

English: “Gold members can cancel any reservation, regardless of insurance status”

Datalog:

IsAuthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "cancel_reservation"),
    ToolResultField("get_reservation_details",
        "membership", "gold").

Checks the membership field from get_reservation_details. Gold overrides the insurance check entirely.

C3: Allow cancel if has insurance

English: “Silver and regular members can only cancel if the reservation has travel insurance”

Datalog:

IsAuthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "cancel_reservation"),
    ToolResultField("get_reservation_details",
        "insurance", "yes").

Any member with insurance can cancel, regardless of tier.

C4: Deny cancel if no insurance, not gold

English: “Deny cancellation if the reservation has no insurance and the member is not gold”

Datalog:

// @deny_message: Only gold members or members with
//   travel insurance can cancel reservations
// @suggestion: Purchase travel insurance or upgrade
//   to gold membership
Unauthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "cancel_reservation"),
    ToolResultField("get_reservation_details",
        "insurance", "no"),
    !ToolResultField("get_reservation_details",
        "membership", "gold").

The @deny_message is shown to the agent when the action is denied. The agent relays this to the customer.

C5: Guard — deny cancel if not looked up

Why: The agent must call get_reservation_details before attempting to cancel. Otherwise it could bypass the insurance check. Gold members are exempt — C2 already lets them cancel without an insurance lookup, so this guard skips them.

Datalog:

// @deny_message: Cannot determine cancellation
//   eligibility without reservation details
// @suggestion: Retrieve reservation details
//   including insurance status
Unauthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "cancel_reservation"),
    !ToolResultField("get_reservation_details",
        "insurance", _),
    !ToolResultField("get_reservation_details",
        "membership", "gold").

The two !ToolResultField(..., _) conjuncts say: the lookup either hasn’t happened, or it returned something other than gold membership. This is a prerequisite guard — a common pattern for policies that depend on runtime data.

Modification Rules

Section titled “Modification Rules”
C6: Allow modify if economy cabin

English: “Economy reservations can be modified by any member”

Datalog:

IsAuthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "update_reservation_flights"),
    ToolResultField("get_reservation_details",
        "cabin", "economy").
C7: Allow modify basic economy for silver/gold

English: “Basic economy reservations can only be modified by silver or gold members”

Datalog:

IsAuthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "update_reservation_flights"),
    ToolResultField("get_reservation_details",
        "cabin", "basic_economy"),
    !ToolResultField("get_reservation_details",
        "membership", "regular").

The membership check is written as a negation (“membership is not regular”) to cover both silver and gold in a single rule. A separate Unauthorized rule (C8) handles the regular case.

C8: Deny modify basic economy for regular

English: “Deny flight modifications on basic economy reservations for regular members”

Datalog:

// @deny_message: Regular members cannot modify
//   basic economy flight reservations
// @suggestion: Upgrade to silver or gold membership
//   for modification capability
Unauthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "update_reservation_flights"),
    ToolResultField("get_reservation_details",
        "cabin", "basic_economy"),
    ToolResultField("get_reservation_details",
        "membership", "regular").
C9: Guard — deny modify if not looked up

Datalog:

// @deny_message: Cannot determine modification
//   eligibility without reservation details
// @suggestion: Retrieve reservation details
//   including cabin class
Unauthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "update_reservation_flights"),
    !ToolResultField("get_reservation_details",
        "cabin", _).

Same pattern as C5 — ensures the agent looks up reservation details before attempting to modify.

C10: Guard — deny basic-economy modify if membership unknown

Why: C7 only allows basic-economy modifications for silver/gold members; C8 only denies them for regular members. If membership hasn’t been looked up yet, neither rule fires — this guard closes that gap so the agent can’t sneak through with a partial lookup.

Datalog:

// @deny_message: Cannot determine modification
//   eligibility without membership information
// @suggestion: Verify membership level before
//   modifying basic economy reservations
Unauthorized(idx) :-
    Actions(idx, a),
    IsTool(a, "update_reservation_flights"),
    ToolResultField("get_reservation_details",
        "cabin", "basic_economy"),
    !ToolResultField("get_reservation_details",
        "membership", _).

Want a complete real-world translation?

Section titled “Want a complete real-world translation?”

The rules above are a minimal pedagogical example. For a full Datalog translation of the tau2 airline policy — with dependency-graph predicates, per-reservation_id scoping, and custom C++ functors for content matching — see tau2-examples/airline/airline_policy.dl in the repo.