pyk.proof.reachability module

class APRFailureInfo(failing_nodes: 'Iterable[int]', pending_nodes: 'Iterable[int]', path_conditions: 'Mapping[int, str]', failure_reasons: 'Mapping[int, str]', models: 'Mapping[int, Iterable[tuple[str, str]]]')[source]

Bases: FailureInfo

failing_nodes: frozenset[int]
failure_reasons: FrozenDict[int, str]
static from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) → APRFailureInfo[source]
models: FrozenDict[int, frozenset[tuple[str, str]]]
path_conditions: FrozenDict[int, str]
pending_nodes: frozenset[int]
print() → list[str][source]
class APRProof(id: str, kcfg: KCFG, terminal: Iterable[int], init: NodeIdLike, target: NodeIdLike, logs: dict[int, tuple[LogEntry, ...]], bmc_depth: int | None = None, bounded: Iterable[int] | None = None, proof_dir: Path | None = None, node_refutations: dict[int, str] | None = None, subproof_ids: Iterable[str] = (), circularity: bool = False, admitted: bool = False, _exec_time: float = 0, error_info: Exception | None = None, prior_loops_cache: dict[int, list[int]] | None = None)[source]

Bases: Proof, KCFGExploration

APRProof and APRProver implement all-path reachability logic, as introduced by A. Stefanescu and others in their paper ‘All-Path Reachability Logic’: https://doi.org/10.23638/LMCS-15(2:5)2019 Note that reachability logic formula phi =>A psi has not the same meaning as CTL/CTL*’s phi -> AF psi, since reachability logic ignores infinite traces. This implementation extends the above with bounded model checking, allowing the user to specify an optional loop iteration bound for each loop in execution.

add_bounded(nid: NodeIdLike) → None[source]
add_exec_time(exec_time: float) → None[source]
as_rule(priority: int = 20) → KRule[source]
bmc_depth: int | None
property bounded: list[Node]
property can_progress: bool
circularity: bool
commit(result: StepResult) → None[source]
construct_node_refutation(node: Node) → RefutationProof | None[source]
property dict: dict[str, Any]
error_info: Exception | None
property exec_time: float
property failing: list[Node]
formatted_exec_time() → str[source]
static from_claim(defn: KDefinition, claim: KClaim, logs: dict[int, tuple[LogEntry, ...]], proof_dir: Path | None = None, bmc_depth: int | None = None, **kwargs: Any) → APRProof[source]
classmethod from_dict(dct: Mapping[str, Any], proof_dir: Path | None = None) → APRProof[source]
static from_spec_modules(defn: KDefinition, spec_modules: KFlatModuleList, logs: dict[int, tuple[LogEntry, ...]], proof_dir: Path | None = None, spec_labels: Iterable[str] | None = None, **kwargs: Any) → list[APRProof][source]
get_refutation_id(node_id: int) → str[source]
init: int
is_bounded(node_id: NodeIdLike) → bool[source]
is_failing(node_id: NodeIdLike) → bool[source]
is_init(node_id: NodeIdLike) → bool[source]
is_pending(node_id: NodeIdLike) → bool[source]
is_refuted(node_id: NodeIdLike) → bool[source]
is_target(node_id: NodeIdLike) → bool[source]
logs: dict[int, tuple[LogEntry, ...]]
property module_name: str
node_refutations: dict[int, RefutationProof]
property own_status: ProofStatus
path_constraints(final_node_id: NodeIdLike) → KInner[source]
property pending: list[Node]
prior_loops_cache: dict[int, list[int]]
prune(node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) → list[int][source]
static read_proof(id: str, proof_dir: Path) → APRProof[source]
static read_proof_data(proof_dir: Path, id: str) → APRProof[source]
refute_node(node: Node) → RefutationProof | None[source]
set_exec_time(exec_time: float) → None[source]
shortest_path_to(node_id: NodeIdLike) → tuple[KCFG.Successor, ...][source]
property summary: CompositeSummary
target: int
unrefute_node(node: Node) → None[source]
write_proof_data() → None[source]
class APRProofBoundedResult(node_id: 'int')[source]

Bases: APRProofResult

class APRProofExtendResult(node_id: 'int', extend_result: 'KCFGExtendResult')[source]

Bases: APRProofResult

extend_result: KCFGExtendResult
class APRProofResult(node_id: 'int')[source]

Bases: StepResult

node_id: int
class APRProofSubsumeResult(node_id: 'int', csubst: 'CSubst')[source]

Bases: APRProofResult

csubst: CSubst
class APRProofTerminalResult(node_id: 'int')[source]

Bases: APRProofResult

class APRProver(proof: APRProof, kcfg_explore: KCFGExplore, execute_depth: int | None = None, cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), counterexample_info: bool = False, always_check_subsumption: bool = True, fast_check_subsumption: bool = False)[source]

Bases: Prover

always_check_subsumption: bool
circularities_module_name: str
counterexample_info: bool
cut_point_rules: Iterable[str]
dependencies_module_name: str
execute_depth: int | None
failure_info() → FailureInfo[source]
fast_check_subsumption: bool
main_module_name: str
nonzero_depth(node: Node) → bool[source]
proof: APRProof
step_proof() → Iterable[StepResult][source]
terminal_rules: Iterable[str]
class APRSummary(id: 'str', status: 'ProofStatus', admitted: 'bool', nodes: 'int', pending: 'int', failing: 'int', vacuous: 'int', stuck: 'int', terminal: 'int', refuted: 'int', bmc_depth: 'int | None', bounded: 'int', subproofs: 'int', formatted_exec_time: 'str')[source]

Bases: ProofSummary

admitted: bool
bmc_depth: int | None
bounded: int
failing: int
formatted_exec_time: str
id: str
property lines: list[str]
nodes: int
pending: int
refuted: int
status: ProofStatus
stuck: int
subproofs: int
terminal: int
vacuous: int