[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: whitewaterssoftwareinfo@xxxxxxxxx*Date*: Thu, 30 May 2019 12:36:58 -0700 (PDT)

Hello everyone, Hypothetically, lets assume that I am designing a circuitry to control a fuel solenoid in a commercial airliner. The circuit takes a number of analog and digital inputs (1 or 0), processes them, and then controls an electric motor which actuates the valve to open or close. At a high level the system is organized as different functional blocks with inputs , outputs, and a certain defined behavior. Unlike a typical computer program each of the blocks is "asynchronous." Different blocks are connected together to get a certain behavior from the system. My goal is to show that the functional blocks work together to produce a deterministic well defined behavior. (eg. it opens when commanded to open, closes when commanded to close, etc.) For reference some inputs/outputs are digital (false=0, or true=1) and others are analog (eg. 0.0 to 1.2345). I have two questions: * Can TLA+ represent "analog" and "digital" signals? (eg. an amplifier with a gain of 2 would take and input of 1.1 and output 2.2, or a digital AND gate would take two 0 or 1 digital inputs and produce a single 0 or 1 digital output) * Is TLA+ a suitable tool to analyze an "asynchronous" analog/digital system similar to what I have described? Thanks Everyone, -Jason White -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0577e562-c902-474d-8757-846ee737be0b%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:

- Prev by Date:
**[tlaplus] Re: Embedding TLA+ in Latex** - Next by Date:
**Re: [tlaplus] Applicability of TLA+ to the design of electronic circuits and systems?** - Previous by thread:
**[tlaplus] Re: how to updating state and return in a definition** - Next by thread:
**Re: [tlaplus] Applicability of TLA+ to the design of electronic circuits and systems?** - Index(es):