// Stitched workflow: differentiation analytics — record → audit → explain decision trail
//
// Full command sequence (run from repo root):
//
//   spanda check examples/workflows/differentiation_audit_trail.sd
//   spanda decision list examples/workflows/differentiation_audit_trail.sd
//   spanda sim examples/workflows/differentiation_audit_trail.sd --record --inject-health-faults
//   spanda audit decisions examples/workflows/differentiation_audit_trail.trace
//   spanda explain decision examples/workflows/differentiation_audit_trail.trace
//   spanda contract verify examples/workflows/differentiation_audit_trail.sd
//   spanda demo differentiation
//
// Docs: docs/overview/signature-capabilities.md · showcase: examples/showcase/differentiation/

robot Scanner001 {
    local_decision_authority [emergency_stop, degraded_mode, obstacle_avoidance];
    requires_central_approval [override_safety_policy, update_firmware];

    sensor gps: GPS;
    sensor lidar: Lidar;
    actuator drive: DifferentialDrive;
    mode safe { }
    safety { max_speed = 1.0 m/s; }

    behavior patrol() {
        loop every 50ms { }
    }
}

decision_tree GPSLossReflex local {
    version = "1.0.0";
    when gps.status == Failed {
        enter degraded_mode;
        trigger emergency_stop;
    }
}

decision_tree ObstacleReflex reflex {
    when obstacle.detected {
        stop_motor;
        cut_actuator_power;
        trigger emergency_stop;
    }
}

offline_policy ScannerOffline {
    max_duration = 15 min;
    policy_version = "1.0.0";
    allowed_actions [pause_mission, return_home, enter_degraded_mode];
    forbidden_actions [disable_safety, start_new_high_risk_mission];
}

recovery_policy AuditRecovery {
    on gps.failed {
        enter degraded_mode;
        reduce_speed 0.5 m/s;
    }
}

continuity_policy AuditContinuity {
    on robot.failed {
        resume from checkpoint;
        reassign mission;
    }
}

assurance_case AuditAssurance {
    evidence simulation_replay;
    evidence health_checks;
}

knowledge_model AuditKnowledge {
    component gps;
    dependency navigation requires [gps];
}
