Propiedad de seguridad de un semáforo: nunca dos verdes, comprobada como «siempre verdadera»

# -*- coding: utf-8 -*-
# Generated by Tangibool (tangibool.python/1). Do not edit by hand; regenerate from the source revision.
# Model: not stated
# Source revision: reference
# Interpretation status: not stated
"""Tangibool evaluator (decision model).

Generated deterministically from the validated Boolean model; it evaluates exactly that
model. It does not establish that the model is a complete, legal, or safe statement of a
real-world rule, and evaluating examples does not verify the rule.

Source revision: reference
Interpretation status: not stated
Exporter: 1.0.0 (format tangibool.python/1; engine 1.0.0; semantics tangibool-semantics/1)
Logic digest: fa408e9369f2c9a12a9907ddd7e7940e4933273ead0218609e6a37a78c743d7d
Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78

Inputs (dict keys, declared order) and generated parameter names:
    'ns_green' -> input_ns_green
    'ew_green' -> input_ew_green

Outputs (declared order) and their functions:
    'ns_go' -> output_ns_go(inputs)
    'ew_go' -> output_ew_go(inputs)
    'conflict' -> output_conflict(inputs)

Assumptions (the declared scope, checked by in_scope(inputs)):
    none; every complete assignment is in scope.

Input contract:
    Every required input must be exactly True or False (type(value) is bool). Missing
    inputs, None, strings, integers (including 0 and 1), and keys that are not declared
    inputs raise InputError before anything is evaluated, including inputs that a
    short-circuiting operator would never read. Results are always bool.

Scope:
    Decision functions raise OutOfScopeError when the inputs violate an assumption; an
    out-of-scope assignment is never turned into a False result. Pass check_scope=False
    to evaluate without the scope check, and use in_scope(inputs) to test it separately.

Usage:

    import tangibool_model as model

    model.evaluate({'ns_green': False, 'ew_green': False})
    # -> {'ns_go': False, 'ew_go': False, 'conflict': False}
    model.output_ns_go({'ns_green': False, 'ew_green': False})
    # -> False
    model.evaluate({'ns_green': 1, 'ew_green': False})
    # raises InputError: 1 is an int, not a bool
"""

import collections.abc as _abc
from typing import Dict, Mapping, Tuple

__all__ = [
    "MODEL_INFO",
    "IDENTIFIER_MAP",
    "INPUT_NAMES",
    "OUTPUT_NAMES",
    "ASSUMPTIONS",
    "InputError",
    "OutOfScopeError",
    "minterm_index",
    "in_scope",
    "evaluate",
    "output_ns_go",
    "output_ew_go",
    "output_conflict",
]

MODEL_INFO = {
    "format": "tangibool.python/1",
    "mode": "decision",
    "model": None,
    "revision": "reference",
    "interpretation": None,
    "exporter": "1.0.0",
    "engine_version": "1.0.0",
    "semantics_version": "tangibool-semantics/1",
    "logic_digest": "fa408e9369f2c9a12a9907ddd7e7940e4933273ead0218609e6a37a78c743d7d",
    "assumptions_digest": "d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78",
    "primary_output": "ns_go",
    "unused_inputs": (),
    "subcircuits": (),
}

# Stable ID -> generated identifier (reversible mapping; names are exact, escaped strings).
IDENTIFIER_MAP = {
    "v_5fbd0000f793": {"kind": "input", "name": "ns_green", "identifier": "input_ns_green"},
    "v_c2f8024e6631": {"kind": "input", "name": "ew_green", "identifier": "input_ew_green"},
    "f_9cfc44c0e181": {"kind": "output", "name": "ns_go", "identifier": "output_ns_go"},
    "f_2f9549d42217": {"kind": "output", "name": "ew_go", "identifier": "output_ew_go"},
    "f_88c1e1772438": {"kind": "output", "name": "conflict", "identifier": "output_conflict"},
}

INPUT_NAMES = ("ns_green", "ew_green")
OUTPUT_NAMES = ("ns_go", "ew_go", "conflict")
ASSUMPTIONS = ()

_DECLARED_INPUTS = frozenset(INPUT_NAMES)
_SCOPE_INPUTS = ()
_ASSUMPTION_FORMULAS = {entry["name"]: entry["formula"] for entry in ASSUMPTIONS}


class InputError(ValueError):
    """Raised when inputs are missing, undeclared, or not exactly True/False.

    Every required input must satisfy type(value) is bool. Missing inputs, None, strings,
    integers (including 0 and 1), and keys that are not declared inputs are rejected before
    anything is evaluated. A missing input is never treated as False. The individual problems
    are listed in the problems attribute.
    """

    def __init__(self, problems):
        self.problems = tuple(problems)
        super().__init__("Invalid inputs: " + "; ".join(self.problems))


class OutOfScopeError(ValueError):
    """Raised when the inputs violate the model's assumptions (its declared scope).

    Outside its assumptions the rule has no decision: this error is never a False result.
    The names of the violated assumptions are in the violated attribute.
    """

    def __init__(self, violated):
        self.violated = tuple(violated)
        details = ", ".join(name + " (" + _ASSUMPTION_FORMULAS.get(name, "?") + ")" for name in self.violated)
        super().__init__(
            "Out of scope: the inputs violate "
            + ("assumption " if len(self.violated) == 1 else "assumptions ")
            + details
            + ". The rule has no decision outside its assumptions; this is not a False result."
        )


def _short_repr(value: object) -> str:
    text = repr(value)
    return text if len(text) <= 60 else text[:57] + "..."


def _checked_inputs(inputs: Mapping[str, bool], required: Tuple[str, ...], check_scope: bool) -> Dict[str, bool]:
    """Validate inputs strictly before anything is evaluated and return a plain copy."""
    if type(check_scope) is not bool:
        raise TypeError("check_scope must be True or False")
    if not isinstance(inputs, _abc.Mapping):
        raise InputError(["inputs must be a mapping from input names to True/False, got " + type(inputs).__name__])
    problems = []
    for key in inputs:
        if type(key) is not str or key not in _DECLARED_INPUTS:
            declared = ", ".join(repr(name) for name in INPUT_NAMES) or "none"
            problems.append("undeclared input " + _short_repr(key) + " (declared inputs: " + declared + ")")
    needed = tuple(required) + (_SCOPE_INPUTS if check_scope else ())
    for name in needed:
        if name not in inputs:
            problems.append("missing required input " + repr(name))
    for key, value in inputs.items():
        if type(key) is str and key in _DECLARED_INPUTS and type(value) is not bool:
            problems.append(
                "input " + repr(key) + " must be True or False (type bool), got "
                + type(value).__name__ + " " + _short_repr(value)
            )
    if problems:
        raise InputError(list(dict.fromkeys(problems)))
    return dict(inputs.items())


def _require_bool_args(function: str, pairs: Tuple[Tuple[str, object], ...]) -> None:
    problems = [
        "argument " + repr(name) + " of " + function + " must be True or False (type bool), got "
        + type(value).__name__ + " " + _short_repr(value)
        for name, value in pairs
        if type(value) is not bool
    ]
    if problems:
        raise InputError(problems)


def minterm_index(*values: bool) -> int:
    """Row index of an assignment over a declared variable order.

    The first value is the most significant bit, so all-False is row 0. Used for indexed
    minterm (sum) and maxterm (product) forms.
    """
    index = 0
    for value in values:
        if type(value) is not bool:
            raise InputError(["minterm_index() takes True/False values, got " + type(value).__name__ + " " + _short_repr(value)])
        index = index * 2 + (1 if value else 0)
    return index


def _scope_values(values: Dict[str, bool]) -> Tuple[Tuple[str, bool], ...]:
    """Value of every enabled, confirmed assumption for validated inputs, in declared order."""
    return ()


def _require_in_scope(values: Dict[str, bool]) -> None:
    violated = tuple(name for name, holds in _scope_values(values) if not holds)
    if violated:
        raise OutOfScopeError(violated)


def in_scope(inputs: Mapping[str, bool]) -> bool:
    """True when the inputs satisfy every assumption (the model's declared scope).

    Requires the inputs the assumptions read; raises InputError for invalid inputs.
    """
    values = _checked_inputs(inputs, (), True)
    return all(holds for _, holds in _scope_values(values))


# ---- Formula bodies (inputs are validated by the public functions below) ----


def _compute_output_ns_go(input_ns_green: bool, input_ew_green: bool) -> bool:
    """Decision output 'ns_go': ns_green AND NOT ew_green"""
    return input_ns_green and (not input_ew_green)


def _compute_output_ew_go(input_ns_green: bool, input_ew_green: bool) -> bool:
    """Decision output 'ew_go': ew_green AND NOT ns_green"""
    return input_ew_green and (not input_ns_green)


def _compute_output_conflict(output_ns_go_value: bool, output_ew_go_value: bool) -> bool:
    """Decision output 'conflict': ns_go AND ew_go (references are passed in once computed: 'ns_go' -> output_ns_go_value, 'ew_go' -> output_ew_go_value)"""
    return output_ns_go_value and output_ew_go_value


# ---- Public API ----


def output_ns_go(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'ns_go' (stable ID f_9cfc44c0e181).

    'ns_go' := ns_green AND NOT ew_green

    Required inputs: 'ns_green', 'ew_green'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("ns_green", "ew_green"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_ns_go_value = _compute_output_ns_go(values["ns_green"], values["ew_green"])
    return output_ns_go_value


def output_ew_go(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'ew_go' (stable ID f_2f9549d42217).

    'ew_go' := ew_green AND NOT ns_green

    Required inputs: 'ns_green', 'ew_green'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("ns_green", "ew_green"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_ew_go_value = _compute_output_ew_go(values["ns_green"], values["ew_green"])
    return output_ew_go_value


def output_conflict(inputs: Mapping[str, bool], *, check_scope: bool = True) -> bool:
    """Decision output 'conflict' (stable ID f_88c1e1772438).

    'conflict' := ns_go AND ew_go

    Required inputs: 'ns_green', 'ew_green'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("ns_green", "ew_green"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_ns_go_value = _compute_output_ns_go(values["ns_green"], values["ew_green"])
    output_ew_go_value = _compute_output_ew_go(values["ns_green"], values["ew_green"])
    output_conflict_value = _compute_output_conflict(output_ns_go_value, output_ew_go_value)
    return output_conflict_value


def evaluate(inputs: Mapping[str, bool], *, check_scope: bool = True) -> Dict[str, bool]:
    """Evaluate every output (declared order); each output is computed once.

    Required inputs: 'ns_green', 'ew_green'.
    Raises InputError for missing, undeclared, or non-bool inputs, and OutOfScopeError
    when check_scope is True and the inputs violate an assumption.
    """
    values = _checked_inputs(inputs, ("ns_green", "ew_green"), check_scope)
    if check_scope:
        _require_in_scope(values)
    output_ns_go_value = _compute_output_ns_go(values["ns_green"], values["ew_green"])
    output_ew_go_value = _compute_output_ew_go(values["ns_green"], values["ew_green"])
    output_conflict_value = _compute_output_conflict(output_ns_go_value, output_ew_go_value)
    return {
        "ns_go": output_ns_go_value,
        "ew_go": output_ew_go_value,
        "conflict": output_conflict_value,
    }

-- Tangibool PostgreSQL export (tangibool.postgresql/1)
-- Target: PostgreSQL 16 or later with typed boolean inputs; tested with PostgreSQL 18.3 (PGlite 0.5.8).
-- Not a claim of compatibility with other SQL dialects.
-- Model: not stated
-- Source revision: reference
-- Interpretation status: not stated
-- Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
-- Logic digest: fa408e9369f2c9a12a9907ddd7e7940e4933273ead0218609e6a37a78c743d7d
-- Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
-- Mode: decision
--
-- Read-only: this file contains only WITH / VALUES / SELECT statements. No DDL, DML,
-- procedures, credentials, network access, or database changes. The expressions are pure
-- Boolean expressions, so their result does not depend on SQL evaluation order.
--
-- NON-NULL INPUT PRECONDITION: NULL is not a truth value of this rule. Every fragment below
-- is defined only when every input column it reads is a non-NULL boolean. The guard template
-- (section 2) marks any NULL input as 'invalid_input' and any row that violates the
-- assumptions as 'out_of_scope', and fills output columns only for 'ok' rows; a NULL in an
-- output column of another row is an envelope marker, not a third truth value. Never wrap
-- the fragments in COALESCE(..., FALSE) or otherwise choose a meaning for unknown inputs.
-- This evaluates the supplied model; it does not show that the model is a complete, legal,
-- or safe statement of a real-world rule.
--
-- Input columns (stable ID: name -> column):
--   v_5fbd0000f793: ns_green -> "in_ns_green"
--   v_c2f8024e6631: ew_green -> "in_ew_green"
-- Output columns:
--   f_9cfc44c0e181: ns_go -> "out_ns_go"
--   f_2f9549d42217: ew_go -> "out_ew_go"
--   f_88c1e1772438: conflict -> "out_conflict"
-- Assumptions (scope K; exported separately and never folded into an output):
--   none; every complete input row is in scope.
-- Named-output references are expanded in place.

-- ----------------------------------------------------------------------------------------------
-- 1. Expression fragments (parenthesised; non-NULL boolean inputs required)
-- ----------------------------------------------------------------------------------------------
--
-- [out_ns_go] output ns_go (stable ID f_9cfc44c0e181)
--   ns_go := ns_green AND NOT ew_green
--   PRECONDITION: "in_ns_green", "in_ew_green" are non-NULL booleans.
--   ("in_ns_green" AND (NOT "in_ew_green"))
--
-- [out_ew_go] output ew_go (stable ID f_2f9549d42217)
--   ew_go := ew_green AND NOT ns_green
--   PRECONDITION: "in_ns_green", "in_ew_green" are non-NULL booleans.
--   ("in_ew_green" AND (NOT "in_ns_green"))
--
-- [out_conflict] output conflict (stable ID f_88c1e1772438)
--   conflict := ns_go AND ew_go
--   PRECONDITION: "in_ns_green", "in_ew_green" are non-NULL booleans.
--   (("in_ns_green" AND (NOT "in_ew_green")) AND ("in_ew_green" AND (NOT "in_ns_green")))
--

-- ----------------------------------------------------------------------------------------------
-- 2. Guard template (read-only SELECT over an inputs list)
-- ----------------------------------------------------------------------------------------------
-- Replace the example rows between the markers with your own rows, or replace the inputs
-- CTE with a SELECT that provides the boolean columns listed in the header. status is
-- 'invalid_input' when any input is NULL, 'out_of_scope' when the assumptions are false, and
-- 'ok' otherwise; output columns are filled only for 'ok' rows (NULL elsewhere is an
-- envelope marker). Assumption columns are shown for rows with complete inputs.
WITH inputs ("row_id", "in_ns_green", "in_ew_green") AS (
  -- tangibool:example-rows:begin
  VALUES
    (1, FALSE, FALSE),
    (2, FALSE, TRUE),
    (3, TRUE, FALSE),
    (4, TRUE, TRUE),
    (5, NULL::boolean, FALSE)
  -- tangibool:example-rows:end
),
checked AS (
  SELECT
    inputs.*,
    CASE
      WHEN "in_ns_green" IS NULL OR "in_ew_green" IS NULL THEN 'invalid_input'
      ELSE 'ok'
    END AS "status"
  FROM inputs
)
SELECT
  "row_id",
  "in_ns_green",
  "in_ew_green",
  "status",
  CASE WHEN "status" = 'ok' THEN ("in_ns_green" AND (NOT "in_ew_green")) END AS "out_ns_go",
  CASE WHEN "status" = 'ok' THEN ("in_ew_green" AND (NOT "in_ns_green")) END AS "out_ew_go",
  CASE WHEN "status" = 'ok' THEN (("in_ns_green" AND (NOT "in_ew_green")) AND ("in_ew_green" AND (NOT "in_ns_green"))) END AS "out_conflict"
FROM checked
ORDER BY "row_id";

; Tangibool SMT-LIB export (tangibool.smtlib/1)
; Profile: SMT-LIB 2.6 Boolean subset (QF_UF): Bool constants, define-fun, let, push/pop, assert, check-sat, echo.
; Tested with Z3 5.1.0 (z3-solver 5.2.0, WebAssembly build).
; Model: not stated
; Source revision: reference
; Interpretation status: not stated
; Exporter: 1.0.0 (engine 1.0.0; semantics tangibool-semantics/1)
; Logic digest: fa408e9369f2c9a12a9907ddd7e7940e4933273ead0218609e6a37a78c743d7d
; Assumptions digest: d58ee1ad38e23e5093e4baa1047b5ae70d6972e08f555e34ac3fa16df63c4a78
; Mode: decision
;
; Reading results: each query block states what sat and unsat mean for its question. A sat
; answer comes with a witness or counterexample (ask for it with (get-model) after sat only);
; unsat settles that scoped query and is solver-checked, not an independently checked proof
; certificate; unknown settles nothing. Blocks are scoped with push/pop, so assertions never
; accumulate across questions. This checks the supplied model, not whether it is a complete,
; legal, or safe statement of a real-world rule.
;
; Symbols (stable ID: name -> symbol):
;   v_5fbd0000f793: ns_green -> in_ns_green
;   v_c2f8024e6631: ew_green -> in_ew_green
;   f_9cfc44c0e181: ns_go -> out_ns_go
;   f_2f9549d42217: ew_go -> out_ew_go
;   f_88c1e1772438: conflict -> out_conflict

(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-logic QF_UF)

; ---- Inputs (declared order)
(declare-const in_ns_green Bool) ; ns_green
(declare-const in_ew_green Bool) ; ew_green

; ---- Outputs (dependencies first)
; output ns_go (stable ID f_9cfc44c0e181): ns_green AND NOT ew_green
(define-fun out_ns_go () Bool (and in_ns_green (not in_ew_green)))
; output ew_go (stable ID f_2f9549d42217): ew_green AND NOT ns_green
(define-fun out_ew_go () Bool (and in_ew_green (not in_ns_green)))
; output conflict (stable ID f_88c1e1772438): ns_go AND ew_go
(define-fun out_conflict () Bool (and out_ns_go out_ew_go))

; ---- Assumptions (the scope K; never folded into an output)
; K: conjunction of the enabled, confirmed assumptions (true when there are none)
(define-fun K () Bool true)

; ---- Definitions only: nothing is asserted and no check is run.
; Add (assert ...) and (check-sat) inside (push 1) ... (pop 1) to ask a question.

ns_go = \mathit{ns\_green} \cdot \overline{\mathit{ew\_green}}
ew_go = \mathit{ew\_green} \cdot \overline{\mathit{ns\_green}}
conflict = \mathit{ns\_go} \cdot \mathit{ew\_go}