Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.stl-robustness

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/stl_robustness.clj5 definitions, 3 theorems

AHoF V6 worked signal-temporal-logic robustness over signed rationals. Two atomic robustness margins x = 1/2 (satisfied) and y = -1/4 (violated) are combined by the STL connectives: conjunction robustness is their minimum (-1/4, so the conjunction is violated), disjunction robustness is their maximum (1/2, satisfied), and negation flips the sign of x (-1/2). The conjunction's minimum is selected through the checked signed-min engine. Scope (measured by the kernel): this module has 3 worked instances (statements about specific values). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.stl-robustness` prints this classification.

Depends onmath.rational.signed.stl

ahof-v6/signal-x :
  → ℚ

ahof-v6/signal-y :
  → ℚ

ahof-v6/and-robustness :
  → ℚ

ahof-v6/or-robustness :
  → ℚ

ahof-v6/not-robustness :
  → ℚ

ahof-v6/and-selects-minimum :
  → validation/signed-min ahof-v6/signal-x ahof-v6/signal-y = ahof-v6/signal-y

ahof-v6/robustness-values :
  → proposition/conjunction (ahof-v6/and-robustness = signed/make 0 1/4) (conjunction)
  where conjunction := proposition/conjunction (ahof-v6/or-robustness = signed/from-nnrat 1/2) (ahof-v6/not-robustness = signed/make 0 1/2)

ahof-v6/stl-robustness :
  → proposition/conjunction (min = ahof-v6/signal-y) (conjunction)
  where conjunction := proposition/conjunction (ahof-v6/and-robustness = signed/make 0 1/4) (proposition/conjunction (ahof-v6/or-robustness = signed/from-nnrat 1/2) (ahof-v6/not-robustness = signed/make 0 1/2))
  where min := validation/signed-min ahof-v6/signal-x ahof-v6/signal-y