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, assume_defined: 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, tuple[int, ...]] | None = None)[source]

Bases: Proof[APRProofStep, APRProofResult], KCFGExploration

Represent an all-path reachability proof.

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]

as_rules(priority: int = 20, direct_rule: bool = False) → list[KRule][source]

bmc_depth: int | None

property bounded: list[Node]

property can_progress: bool

property circularities_module_name: str

circularity: bool

commit(result: APRProofResult) → None[source]

construct_node_refutation(node: Node) → RefutationProof | None[source]

property dependencies_module_name: str

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) → list[APRProof][source]

get_refutation_id(node_id: int) → str[source]

get_steps() → list[APRProofStep][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]

nonzero_depth(node: Node) → bool[source]

property one_line_summary: str

property own_status: ProofStatus

path_constraints(final_node_id: NodeIdLike, sort_with: KDefinition | None = None) → KInner[source]

property pending: list[Node]

prior_loops_cache: dict[int, tuple[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]

property rule_id: str

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', prior_loops_cache_update: 'tuple[int, ...]')[source]: Bases: APRProofResult

class APRProofExtendAndCacheResult(node_id: int, prior_loops_cache_update: tuple[int, ...], extension_to_apply: KCFGExtendResult, extension_to_cache: KCFGExtendResult)[source]

Bases: APRProofExtendResult

Proof extension to be cached.

extension_to_cache: KCFGExtendResult

class APRProofExtendResult(node_id: int, prior_loops_cache_update: tuple[int, ...], extension_to_apply: KCFGExtendResult)[source]

Bases: APRProofResult

Proof extension to be applied.

extension_to_apply: KCFGExtendResult

class APRProofResult(node_id: 'int', prior_loops_cache_update: 'tuple[int, ...]')[source]

Bases: object

node_id: int

prior_loops_cache_update: tuple[int, ...]

class APRProofStep(node: 'KCFG.Node', target: 'KCFG.Node', proof_id: 'str', bmc_depth: 'int | None', use_cache: 'NodeIdLike | None', module_name: 'str', shortest_path_to_node: 'tuple[KCFG.Node, ...]', prior_loops_cache: 'FrozenDict[int, tuple[int, ...]]', circularity: 'bool', nonzero_depth: 'bool', circularity_rule_id: 'str')[source]

Bases: object

bmc_depth: int | None

circularity: bool

circularity_rule_id: str

module_name: str

node: KCFG.Node

nonzero_depth: bool

prior_loops_cache: FrozenDict[int, tuple[int, ...]]

proof_id: str

shortest_path_to_node: tuple[KCFG.Node, ...]

target: KCFG.Node

use_cache: NodeIdLike | None

class APRProofSubsumeResult(node_id: 'int', prior_loops_cache_update: 'tuple[int, ...]', csubst: 'CSubst')[source]

Bases: APRProofResult

csubst: CSubst

class APRProofTerminalResult(node_id: 'int', prior_loops_cache_update: 'tuple[int, ...]')[source]: Bases: APRProofResult

class APRProofUseCacheResult(node_id: int, prior_loops_cache_update: tuple[int, ...], cached_node_id: NodeIdLike)[source]

Bases: APRProofResult

Proof extension to be applied using the extension cache.

cached_node_id: NodeIdLike

class APRProver(kcfg_explore: KCFGExplore, execute_depth: int | None = None, cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), counterexample_info: bool = False, fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, assume_defined: bool = False)[source]

Bases: Prover[APRProof, APRProofStep, APRProofResult]

assume_defined: bool

close() → None[source]

counterexample_info: bool

cut_point_rules: Iterable[str]

direct_subproof_rules: bool

execute_depth: int | None

failure_info(proof: APRProof) → FailureInfo[source]

fast_check_subsumption: bool

init_proof(proof: APRProof) → None[source]

kcfg_explore: KCFGExplore

main_module_name: str

step_proof(step: APRProofStep) → list[APRProofResult][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