Pith. sign in

REVIEW 3 major objections 4 minor 1 cited by

LLM-based Property-based Test Generation for Guardrailing Cyber-Physical Systems

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read ChekProp claims that one LLM pass over a cyber-physical system's documentation, source code, and example unit test can extract its safety-relevant properties and generate property-based tests that verify them, and that the same assertions…

desk verdict A reasonable extension of LLM-based property-based testing to CPS with a sensible list of challenges, but the headline relevance metrics are inflated by counting non-equivalent properties as matches. read the letter →

arxiv 2505.23549 v2 pith:J3PND552 submitted 2025-05-29 cs.SE

Khashayar Etemadi , Marjan Sirjani , Mahshid Helali Moghadam , Per Strandberg , Paul Pettersson This is my paper
classification cs.SE
keywords property-basedtestingLLM4SEcyber-physicalsystemssafetyguardrailstestgenerationHypothesisruntimemonitoringRaspberryPi
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

ChekProp claims that one LLM pass over a cyber-physical system's documentation, source code, and example unit test can extract its safety-relevant properties and then generate property-based tests — tests that check a general rule across many generated inputs rather than one fixed example — verifying those properties. Across nine Python CPS programs, the LLM-extracted properties matched manually crafted ground-truth properties at 94% recall and 72% precision: almost every hand-written safety rule was rediscovered, at the price of some extra irrelevant properties. The generated tests were executable with minor fixes for 47% of the relevant properties, and 85% of them covered most partitions of the input space. The paper's further claim is that the same property assertions, with the input generator dropped and the test body replaced by a monitor, can run after deployment as guardrails that block unsafe commands. A sympathetic reader should care because property definition is the bottleneck in CPS safety assurance, and this is a concrete proposal to automate it end to end.

What carries the argument

The central object is the property-based test itself, understood as a three-part device: an input generator that draws from the input space, a test body that collects system state, and test assertions that encode the property. ChekProp's load-bearing mechanism is the prompt that assembles the system's natural-language description together with its Python code and one unit test, instructing the LLM to first extract properties and then write hypothesis-based tests against them. The paper's runtime-guardrail argument rides on the same three-part anatomy, read as a monitor: input generation is supplied by the live system, the test body becomes the data collector, and the assertions become the guards that raise warnings on violation.

What would settle it

Ask annotators who did not write the ground-truth properties to independently and blindly label each of the 25 extracted properties as a match or non-match with the 19 ground-truth properties, and compare their precision and recall with the reported 72% and 94%. A drop of more than a few points would show the relevance numbers depend on the authors' own equivalence judgment. A stronger external test: run ChekProp on a CPS whose required safety properties are fixed by an independent standard or specification and count how many mandated properties it extracts.

Watch

Extended reading notes

Core claim

The paper's claim, stated on its own terms, is that an LLM prompted with the four-part structure of natural-language description, CPS source code, one example unit test, and generation instructions produces property-based tests whose properties match manually crafted ones: 18 of 19 ground-truth properties were recovered in identical or equivalent form, three additional relevant properties were found that the human-graded sets omitted, and only one ground-truth property, tied to documentation the prompt lacked, was missed. For the 21 properties judged relevant, 47% of the generated tests reached syntactic and semantic correctness with less than a minute of manual modification, and 85% exercised most input-space partitions. The authors additionally argue that the three-component anatomy of a property-based test — input generator, test body, test assertion — is what makes runtime guardrailing possible: at deployment the generator is discarded, the test body becomes a monitor sitting between controller and plant, and the assertions become guards that can intercept and block unsafe commands.

Load-bearing premise

For seven of the nine programs, the ground-truth properties against which ChekProp is scored were written by the same authors who then judged whether the tool's differently-worded properties count as matches; if that self-authored oracle and its generous equivalence judgments are biased, the 94% recall and 72% precision overstate how well the tool extracts relevant properties.

Editorial extensions

If this is right

  • Property extraction, currently a manual bottleneck in CPS safety assurance, becomes largely automatable: 18 of 19 hand-written properties across nine programs were recovered by the LLM, leaving humans to review rather than author the property set.
  • The same generated assertions do double duty: they serve as design-time tests, and with the input generator removed they are meant to become runtime monitors that can intercept unsafe commands before they reach the physical system.
  • Because the tool found three relevant properties (Pr4, Pr8, Pr26) that the human-crafted sets omitted, automated extraction can check and improve manual property engineering rather than only replace it.
  • The failure analysis identifies two concrete improvement levers for LLM-based CPS testing: including mocking examples in the prompt, and supplying documentation and code from all parts of the project rather than a single class.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The runtime-monitoring half of the pipeline is described but not implemented or measured; a natural next experiment is to deploy the generated assertions on one of the nine programs with injected faults and measure detection latency and false-alarm rate.
  • All nine subjects are discrete, event-loop-style Python programs whose plants are mocked or simulated; a system with continuous dynamics, sensor noise, or nondeterministic timing would test whether property extraction and input-space coverage behave as well outside this shape of program.
  • The 72% precision figure probably depends on how generously 'equivalent but slightly different formulations' are counted; a stricter matching protocol would likely lower precision and give practitioners a better estimate of the noise they must filter.
  • A relevance filter that scores extracted properties — for example, by whether they check application-level behavior rather than implementation internals, which would have flagged Pr13, Pr16, Pr19, and Pr22 as not useful — would be a direct way to raise precision automatically.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes ChekProp, an approach that uses an LLM to extract properties from natural-language documentation, Python source code, and unit tests of cyber-physical systems, and then generates property-based tests (PBTs) that verify those properties. The approach also sketches a runtime monitoring phase. The evaluation covers nine programs (TCS, PCS, six Raspberry Pi/gpiozero projects, and the gpiozero InputDevice class) and reports relevance (94% recall, 72% precision against manually crafted ground-truth properties), executability (47% of PBTs for 21 relevant properties run with less than one minute of manual changes), and effectiveness (85% cover most input-space partitions). The central claim is that ChekProp extracts relevant properties comparable to manually crafted ones and generates executable, effective PBTs.

Significance. If the reported numbers were secure, the paper would demonstrate a useful step toward automating safety-property extraction for CPS: the code and prompts are publicly available, the design separates design-time PBT generation from runtime monitoring, and the approach is evaluated on a mix of literature benchmarks and real Raspberry Pi programs. The main limitation is that the quantitative evidence is preliminary and rests on subjective judgments: the ground-truth properties for seven of nine programs are authored by the same researchers who judge matches, and the 'equivalent but slightly different' matching criterion is applied to logically non-equivalent properties. The PBT-quality numbers inherit this subjectivity. With an independent oracle and a tighter equivalence criterion, the approach could become a credible contribution; as presented, the central claim is not yet established.

major comments (3)
  1. [§4.3, Table 2 (Pr1, Pr2, Pr6)] The Group2 matches in Table 2 are not equivalent formulations. Pr1's ground truth is 'if temp > 23, heater should not be heating' but ChekProp's property is 'heater activated if temp < 21'; neither implication holds, since a heater can be off at temp 20 or on at temp 24. Pr2 has the same structure. Pr6's ground truth 'cylinders should not move simultaneously' is not equivalent to ChekProp's 'movement follows a specific order'; mutual exclusion does not entail a fixed order. Reclassifying these three as non-matches changes recall from 18/19 (94%) to 15/19 (79%) and precision from 18/25 (72%) to 15/25 (60%). This directly weakens the paper's central claim that ChekProp's extracted properties are comparable to manually crafted ones.
  2. [§4.3, §4.4] The ground-truth properties for P3-P9 are manually defined by the authors who also perform the relevance matching, and the judgment that Pr4, Pr8, and Pr26 are 'relevant but neglected' is likewise self-assessment. There is no independent annotation, inter-rater reliability, or external oracle for these programs. Because the relevance labels drive both the recall/precision metrics and the RQ2 subset of 21 properties, the reported 94%/72% and the RQ2 percentages could reflect the authors' generous equivalence criterion rather than ChekProp's actual performance. An independent annotator or a public benchmark with agreed ground truth is needed.
  3. [§3, §4.2, §4.4] For programs without an external specification (P3-P9), the LLM derives properties from the code and documentation and the generated PBTs then verify those properties against the same code; this is partially self-referential. Passing PBTs show consistency between the inferred property and the implementation, not that the property is the correct safety requirement. The paper should acknowledge this threat and, where possible, validate extracted properties against an independent safety specification or check whether the PBTs detect injected faults.
minor comments (4)
  1. [§3 opening] The word 'gaurdrailing' should be 'guardrailing'.
  2. [Table 2, rows Pr14-Pr15] 'Thermin' should be 'Theremin'.
  3. [§4.3 II] 'distinct different formulations' should likely read 'slightly different formulations'.
  4. [Figure 1] The tool name appears inconsistently as ChekProp and ChekPROP; please unify the spelling.

Circularity Check

2 steps flagged · score 5.0 of 10

Relevance recall of 94% is partly an artifact of the authors' own ground-truth authorship and a loose 'equivalent but slightly different' counting rule.

  1. self definitional [§4.3 RQ1 Methodology and Results; Table 2]
    "For the remaining programs (P3-P9), we manually define the ground-truth properties. ... Group2 consists of 3 properties that are present among ground-truth and ChekProp extracted properties in equivalent but slightly different forms (Pr1, Pr2, and Pr6); ... These properties are relevant, since they are present among the manually crafted properties."

    The headline 'recall of ChekProp is 94% (18/19)' is produced by a counting rule that the same authors both wrote and applied. Table 2 pairs Pr1 ground truth 'If the room is warm (temp > 23), the HC unit should not be heating the room' with ChekProp's 'Heater should be activated if the temperature drops below 21°C'; these do not entail each other, and the Pr2 and Pr6 pairs are similarly not logical equivalents. Because relevance is defined as 'present among the manually crafted properties' and both the manual ground truth and the equivalence judgment are internal to the author team, the 18/19 and 18/25 counts are partly artifacts of that self-defined equivalence rule rather than an independent measure of property extraction.

  2. other [§4.4 RQ2 Methodology]
    "For evaluating the quality of PBTs generated by ChekProp, we examine the PBTs that test the 21 relevant properties according to our analysis in the RQ1 experiment (see subsection 4.3)."

    The executability (47%) and effectiveness (85%) results are computed only over the 21 properties selected by the same RQ1 process, which includes the three Group2 properties counted as 'equivalent but slightly different' and the three properties the authors themselves label as 'relevant ... neglected in manually crafted properties' (Pr4, Pr8, Pr26). Thus the RQ2 percentages are conditional on the same self-authored relevance filter that drives RQ1; they do not provide an independent check of PBT quality, and they inherit the equivalence-rule artifact from Table 2.

full rationale

The core pipeline—prompting an LLM with CPS documentation, code, and unit tests, then generating PBTs—is not itself a circular derivation: no equation in the paper is assumed as its own conclusion, and no fitted parameter is renamed as a prediction. The circularity sits in the evaluation oracle that supports the central claim. The paper's own text shows that for P3-P9 the ground-truth properties are manually defined by the same authors who then judge which extracted properties count as matching, and that the Group2 rule declares 'equivalent but slightly different' properties (Pr1, Pr2, Pr6) to be hits even though the quoted formulations are logically distinct. Consequently, the reported 94% recall and 72% precision are partly constructed by that self-defined equivalence judgment, and RQ2's 47%/85% figures inherit the same filter because they are computed only on the 21 properties selected in RQ1. There is still independent content: 15 exact matches and several plausibly relevant extracted properties remain even if the three Group2 pairs are reclassified, so the paper is not wholly circular; however, the headline 'comparable to manually crafted properties' needs an independent or more conservatively applied oracle before it is supported. The use of Moradi et al. [12] for P1/P2 also involves an overlapping author, further weakening the 'external ground truth' framing, though it supplies only part of the dataset.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The central quantitative results depend on the faithfulness of the author-written Python CPS implementations, the correctness of the self-authored ground truth, and the untested assumption that PBT assertions transfer from mocked design-time tests to runtime guardrails. No parameters are fitted to data, but the evaluation thresholds and matching criteria are hand-chosen.

free parameters (2)
  • Executability time thresholds (1 and 3 minutes) = HIGH < 1 min; MED 1-3 min; LOW > 3 min
    These hand-chosen thresholds in Section 4.4 determine the reported 47% executability rate; a different threshold would change the headline percentage.
  • Relevance matching criteria for "equivalent but slightly different" forms = Group2: Pr1, Pr2, Pr6 counted as matches
    The subjective decision to count paraphrased properties as matches in Table 2 directly sets recall at 18/19 (94%); a stricter matching rule would lower it.
assumptions (4)
  • domain assumption The Python implementations of TCS and PCS are faithful translations of the original Rebeca models from [12].
    Section 4.2 states "We carefully implement TCS and PCS in Python to make them amenable to PBT generation by ChekProp." If the translation introduced semantic drift, the ground-truth comparison would be invalid.
  • ad hoc to paper The manually crafted ground-truth properties for P3-P9 are correct and complete.
    Section 4.3: "For the remaining programs (P3-P9), we manually define the ground-truth properties." These authors are also the evaluators, so the oracle is not independent.
  • domain assumption PBTs that pass on a mocked environment will detect unsafe states on the real deployed CPS.
    Section 3.6 assumes the PBT test body and assertions can be reused as a runtime monitor without additional validation; no experiment supports this.
  • domain assumption The nine programs in the dataset are representative of CPSs in general.
    Section 4.2: dataset consists of two model-based examples, six Raspberry Pi projects, and one library class; limited external validity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of LLM-based Property-based Test Generation for Guardrailing Cyber-Physical Systems." pith.science (2026). https://pith.science/paper/J3PND552

@misc{pith2026250523549,
  author       = {Pith},
  title        = {Pith review of: LLM-based Property-based Test Generation for Guardrailing Cyber-Physical Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J3PND552}},
  note         = {Machine review of arXiv:2505.23549}
}
read the original abstract

Cyber-physical systems (CPSs) are complex systems that integrate physical, computational, and communication subsystems. The heterogeneous nature of these systems makes their safety assurance challenging. In this paper, we propose a novel automated approach for guardrailing cyber-physical systems using property-based tests (PBTs) generated by Large Language Models (LLMs). Our approach employs an LLM to extract properties from the code and documentation of CPSs. Next, we use the LLM to generate PBTs that verify the extracted properties on the CPS. The generated PBTs have two uses. First, they are used to test the CPS before it is deployed, i.e., at design time. Secondly, these PBTs can be used after deployment, i.e., at run time, to monitor the behavior of the system and guardrail it against unsafe states. We implement our approach in ChekProp and conduct preliminary experiments to evaluate the generated PBTs in terms of their relevance (how well they match manually crafted properties), executability (how many run with minimal manual modification), and effectiveness (coverage of the input space partitions). The results of our experiments and evaluation demonstrate a promising path forward for creating guardrails for CPSs using LLM-generated property-based tests.

Figures

Figures reproduced from arXiv: 2505.23549 by the authors.

Figure 1
Figure 1. Overview of the proposed two-phase approach. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. The natural language document that describes a Pneumatic Control Sys [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. As illustrated in the [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 3
Figure 3. Figure 3: The structure of initial prompt used by ChekProp for generating an initial set of PBTs [PITH_FULL_IMAGE:figures/full_fig_p008_3.png]
Figure 4
Figure 4. Figure 4: The prompt used by ChekProp to generate PBTs for the line following robot program [PITH_FULL_IMAGE:figures/full_fig_p029_4.png]
Figure 5
Figure 5. Figure 5: The prompt used by ChekProp to generate PBTs for the InputDevice class [PITH_FULL_IMAGE:figures/full_fig_p030_5.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts

    cs.SE 2026-07 conditional novelty 4.0 of 10

    LLM-generated Solidity test properties catch most of the mutants that human-written properties catch on average, and match human quality on the LibBit contract.

Reference graph

Works this paper leans on

101 extracted references · 74 canonical work pages · cited by 1 Pith paper

  1. [1]

    In: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering

    Alshahwan, N., Chheda, J., Finogenova, A., Gokkaya, B., Harman, M., Harper, I., Marginean, A., Sengupta, S., Wang, E.: Automated unit test improvement using large language models at meta. In: Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering. pp. 185–196 (2024)

    2024

  2. [2]

    In: Companion Proceedings of the 32nd ACM In- ternational Conference on the Foundations of Software Engineering

    Chen, Y., Hu, Z., Zhi, C., Han, J., Deng, S., Yin, J.: Chatunitest: A framework for llm-based test generation. In: Companion Proceedings of the 32nd ACM In- ternational Conference on the Foundations of Software Engineering. pp. 572–576 (2024)

    2024

  3. [3]

    In: Proceedings of the fifth ACM SIGPLAN international con- ference on Functional programming

    Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of haskell programs. In: Proceedings of the fifth ACM SIGPLAN international con- ference on Functional programming. pp. 268–279 (2000)

    2000

  4. [4]

    Etemadi, K.e.a.: Chekprop (2025),https://github.com/khesoem/ChekProp

    2025

  5. [5]

    ACM SIGSOFT Software Engineering Notes22(4), 74–80 (1997)

    Fink, G., Bishop, M.: Property-based testing: a new approach to testing for assur- ance. ACM SIGSOFT Software Engineering Notes22(4), 74–80 (1997)

    1997

  6. [6]

    arXiv preprint arXiv:2501.19085 (2025)

    Giagnorio, A., Martin-Lopez, A., Bavota, G.: Enhancing code generation for low- resource languages: No silver bullet. arXiv preprint arXiv:2501.19085 (2025)

    arXiv 2025

  7. [7]

    ISO 25000: ISO/IEC 25010 - System and software quality models (2019), available at https://iso25000.com/index.php/en/iso-25000-standards/iso-25010

    2019

  8. [8]

    arXiv preprint arXiv:2406.00515 (2024)

    Jiang, J., Wang, F., Shen, J., Kim, S., Kim, S.: A survey on large language models for code generation. arXiv preprint arXiv:2406.00515 (2024)

    arXiv 2024

Show all 101 references
  1. [9]

    In: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)

    Kang, S., Yoon, J., Yoo, S.: Large language models are few-shot testers: Explor- ing llm-based general bug reproduction. In: 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). pp. 2312–2323. IEEE (2023)

    2023

  2. [10]

    arXiv preprint arXiv:2409.06450 (2024)

    Lu, Q., Wang, X., Jiang, Y., Zhao, G., Ma, M., Feng, S.: Multimodal large language model driven scenario testing for autonomous vehicles. arXiv preprint arXiv:2409.06450 (2024)

    2024 arXiv

  3. [11]

    Journal of Open Source Software4(43), 1891 (2019)

    MacIver, D.R., Hatfield-Dodds, Z., et al.: Hypothesis: A new approach to property- based testing. Journal of Open Source Software4(43), 1891 (2019)

    2019

  4. [12]

    Journal of Logical and Algebraic Methods in Programming139, 100965 (2024)

    Moradi, F., Asadollah, S.A., Pourvatan, B., Moezkarimi, Z., Sirjani, M.: Crystal framework: Cybersecurity assurance for cyber-physical systems. Journal of Logical and Algebraic Methods in Programming139, 100965 (2024)

    2024

  5. [13]

    In: 2024 2nd International Conference on Foundation and Large Language Models (FLLM)

    Petrovic,N.,Lebioda,K.,Zolfaghari,V.,Schamschurko,A.,Kirchner,S.,Purschke, N., Pan, F., Knoll, A.: Llm-driven testing for autonomous driving scenarios. In: 2024 2nd International Conference on Foundation and Large Language Models (FLLM). pp. 173–178. IEEE (2024)

    2024

  6. [14]

    arXiv preprint arXiv:2404.01558 (2024) Title Suppressed Due to Excessive Length 27

    Rahman, T., Zhu, Y.: Automated user story generation with test case specification using large language model. arXiv preprint arXiv:2404.01558 (2024) Title Suppressed Due to Excessive Length 27

    2024 arXiv

  7. [15]

    raspberrypi.org/en/projects

    Raspberry Pi Team: Raspberry Pi Project Selector (2025), https://projects. raspberrypi.org/en/projects

    2025

  8. [16]

    Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday pp

    Sirjani, M., Khamespanah, E.: On time actors. Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday pp. 373–392 (2016)

    2016

  9. [17]

    (2025),https: //github.com/gpiozero/gpiozero

    gpiozero Team: A simple interface to gpio devices with raspberry pi. (2025),https: //github.com/gpiozero/gpiozero

    2025

  10. [18]

    ACM SIGSOFT Software Engineering Notes 30(5), 253–262 (2005)

    Tillmann, N., Schulte, W.: Parameterized unit tests. ACM SIGSOFT Software Engineering Notes 30(5), 253–262 (2005)

    2005

  11. [19]

    In: 2024 IEEE International Conference on Source Code Analysis and Manipulation (SCAM)

    Tiwari, D., Gamage, Y., Monperrus, M., Baudry, B.: Proze: Generating parameter- ized unit tests informed by runtime data. In: 2024 IEEE International Conference on Source Code Analysis and Manipulation (SCAM). pp. 166–176. IEEE (2024)

    2024

  12. [20]

    Vikram, V., Lemieux, C., Sunshine, J., Padhye, R.: Can large language models write good property-based tests? arXiv preprint arXiv:2307.04346 (2023)

    2023 arXiv

  13. [21]

    IEEE Transactions on Software Engineering (2024)

    Wang, J., Huang, Y., Chen, C., Liu, Z., Wang, S., Wang, Q.: Software testing with large language models: Survey, landscape, and vision. IEEE Transactions on Software Engineering (2024)

    2024

  14. [22]

    arXiv preprint arXiv:2310.01361 (2023) 28 K

    Wang, L., Ling, Y., Yuan, Z., Shridhar, M., Bao, C., Qin, Y., Wang, B., Xu, H., Wang, X.: Gensim: Generating robotic simulation tasks via large language models. arXiv preprint arXiv:2310.01361 (2023) 28 K. Etemadi et al. Appendix A: Example Prompts and Generated PBTs Here we p...

    2023 arXiv

  15. [23]

    The following is a description of a line following robot. 2

  16. [24]

    {Natural Language Description}

  17. [26]

    You should generate property based tests for this code

    The following code implements this line following robot using the gpiozero library for Raspberry Pi programs. You should generate property based tests for this code. 6

  18. [27]

    class LineFollowingRobot(Robot):

  19. [28]

    def __init__(self, left, right, left_seonsor_pin=17, right_sensor_pin=27, speed=0.65):

  20. [29]

    super().__init__(left, right)

  21. [30]

    self.left_sensor = LineSensor(left_seonsor_pin)

  22. [31]

    self.right_sensor = LineSensor(right_sensor_pin)

  23. [32]

    self.source = self.motor_speed() 15

  24. [33]

    def motor_speed(self):

  25. [34]

    left_detect = int(self.left_sensor.value)

  26. [35]

    right_detect = int(self.right_sensor.value)

  27. [36]

    if left_detect == 0 and right_detect == 0:

  28. [37]

    if left_detect == 0 and right_detect == 1:

  29. [38]

    if left_detect == 1 and right_detect == 0:

  30. [39]

    print(right_mot, left_mot)

  31. [40]

    yield right_mot * self.speed, left_mot * self.speed 33

  32. [41]

    self.left_sensor.close()

  33. [42]

    self.right_sensor.close()

  34. [44]

    The following is a unit test for this system class: 43

  35. [45]

    raise PinInvalidState(

  36. [46]

    def test_left_sensor_activation_moves_right_motor():

  37. [48]

    Device.pin_factory = MockFactory() 49

  38. [49]

    self._inactive_state = not self._active_state 50

  39. [50]

    with LineFollowingRobot(Motor(2, 3, enable=4, pwm=False),

  40. [51]

    Motor(5, 6, enable=7, pwm=False),

  41. [52]

    left_seonsor_pin=8, right_sensor_pin=9, speed=1) as lfr: 53

  42. [54]

    If :data:`True`, the device uses a pull-up resistor to set the GPIO pin

  43. [55]

    lfr.left_sensor.pin.drive_high()

  44. [57]

    assert lfr.right_motor.value == 1

  45. [59]

    ------------------------------------------------------------------------------------------------------------------------------------

  46. [61]

    Fig.4: The prompt used byChekProp to generate PBTs for the line following robot program

    Based on the extracted properties and your understanding of the code, use the hypothesis library to generate property based tests. Fig.4: The prompt used byChekProp to generate PBTs for the line following robot program. 30 K. Etemadi et al

  47. [62]

    The following is the description of the InputDevice class in the gpiozero library. 2

  48. [63]

    The constructor adds the optional *pull_up* parameter to specify how the pin should be pulled by the internal resistors

    InputDevice class represents a generic GPIO input device.This class extends :class:`GPIODevice` to add facilities common to GPIO input devices. The constructor adds the optional *pull_up* parameter to specify how the pin should be pulled by the internal resistors. The :attr:`i...

  49. [64]

    :type pin: int or str

  50. [65]

    See :ref:`pin-numbering` for valid pin numbers

    The GPIO pin that the device is connected to. See :ref:`pin-numbering` for valid pin numbers. If this is :data:`None` a :exc:`GPIODeviceError` will be raised. :type pull_up: bool or None :param pull_up: If :data:`True`, the pin will be pulled high with an internal resistor. If...

  51. [66]

    :type active_state: bool or None

  52. [67]

    :param active_state:

  53. [68]

    If :data:`False`, the input polarity is reversed: when the hardware pin state is ``HIGH``, the software pin state is ``LOW``

    If :data:`True`, when the hardware pin state is ``HIGH``, the software pin is ``HIGH``. If :data:`False`, the input polarity is reversed: when the hardware pin state is ``HIGH``, the software pin state is ``LOW``. Use this parameter to set the active state of the underlying pi...

  54. [69]

    :type pin_factory: Factory or None

  55. [70]

    See :doc:`api_pins` for more information (this is an advanced feature

  56. [71]

    which most users can ignore)

  57. [73]

    The following code is the implemention of the InputDevice class of the gpiozero library. 21

  58. [74]

    class InputDevice(GPIODevice):

  59. [75]

    def __init__(self, pin=None, *, pull_up=False, active_state=None,

  60. [76]

    super().__init__(pin, pin_factory=pin_factory)

  61. [77]

    self.pin.function = 'input'

  62. [78]

    pull = {None: 'floating', True: 'up', False: 'down'}[pull_up]

  63. [79]

    if self.pin.pull != pull:

  64. [80]

    self.pin.pull = pull

  65. [81]

    if active_state is None:

  66. [83]

    f'Pin {self.pin.info.name} is defined as floating, but '

  67. [84]

    active_state

    f'"active_state" is not defined')

  68. [85]

    self._active_state = bool(active_state)

  69. [86]

    if active_state is not None:

  70. [87]

    f'Pin {self.pin.info.name} is not floating, but '

  71. [88]

    active_state

    f'"active_state" is not None')

  72. [89]

    self._active_state = False if pull_up else True

  73. [90]

    pull = self.pin.pull

  74. [91]

    if pull == 'floating':

  75. [92]

    return pull == 'up' 62

  76. [94]

    The following is a unit test for this class: 66

  77. [95]

    def test_input_initial_values():

  78. [96]

    # Create a MockFactory and use it as pin_factory on Device

  79. [97]

    Device.pin_factory = MockFactory()

  80. [98]

    with InputDevice(4, pull_up=True) as device:

  81. [99]

    assert repr(device).startswith('<gpiozero.InputDevice object')

  82. [100]

    assert device.pin.function == 'input'

  83. [101]

    assert device.pin.pull == 'up'

  84. [102]

    assert device.pull_up

  85. [103]

    assert repr(device) == '<gpiozero.InputDevice object closed>'

  86. [104]

    with InputDevice(4, pull_up=False) as device:

  87. [105]

    assert device.pin.pull == 'down'

  88. [106]

    assert not device.pull_up

  89. [107]

    ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

  90. [108]

    Generate property based tests for this system following the steps below:

  91. [109]

    Based on the given description and code, extract the properties of the system

  92. [110]

    Use the unit tests to understand the behavior and interface of the code

  93. [111]

    Fig.5: The prompt used by ChekProp to generate PBTs for theInputDevice class

    Based on the extracted properties and your understanding of the code, use the hypothesis library to generate property based tests. Fig.5: The prompt used by ChekProp to generate PBTs for theInputDevice class

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.