"Be careful with not generating specs and models with state spaces too big that make model checking impossible."Yes, I come from an engineering background, as in electrical, automation and functional safety, and been using state machines in a practical way for many years - there are a few techniques to lessen the size of any given FSM, the first one being if you can break out a conditioning FSM to manage mode (eg Local. Off, Auto, Remote is a common circumstance in process plant, or similar for machinery.)Then there is the system and subsystem breakdown concept, a trivial example being do you do an FSM for one motor that can run forward or reverse as a single FSM, or do you have an FSM that is for a motor that only runs in one direction, and interconnect two of them for a reversing motor - because forward and reverse are mutually exclusive that is potentially better as two machines, even though it is one object. Do this and break out even just local/remote as well and you can be up to one sixteenth the number of states (more or less) straight away. Big difference.Then at a larger scale sometimes you might build layers of hierarchy, with one to many and many to one FSM intermediaries between the layers, that do not directly relate to any real world objects - synthetic FSM for convenience.You can also have nested FSM, where a transition might be dependant on the result of an FSM sub-system, it's like a subroutine - sometimes useful for more batching like applications where you might have an optional detour via a subsequence, for warm-up or cleaning, that might not always be done, eg just first batch run of the day, or when cold.And so on, many small tricks I have evolved over the years for practical use.I find that the black art is the optimal system and subsystem decomposition. It is hard to teach and is best learned by trying and failing a little, like learning to ride a bike.GarethOn Thu, May 25, 2023 at 9:49 PM Felipe Oliveira Carvalho <feli...@xxxxxxxxx> wrote:FelipeBe careful with not generating specs and models with state spaces too big that make model checking impossible.PlusCal is an imperative language that is used as a starting point in TLA+ code generation. The generated code describes the state transitions modeling the program counter and stack as part of the model state.You could look at that or if your system already produces some kind of state transition specification, generating the code yourself might not be that hard.
----On Thu, May 25, 2023 at 5:09 AM Gareth Smith <anything...@xxxxxxxxx> wrote:yeah I am looking as well - I have an application that lets you specify state based behaviour for industrial automation and functional safety as an executable specification, and part of this is once the specification is data then formal methods translation looks do-ableSo I am already generating functionality in a few different languages of code for export OK, but not TLA+ yetCurrently I end up in negotiations with a prospective buyer, so maybe I won't get there first, but if there was a starting point of a codebase or similar I could leverage off, that would be great.--I am currently working on a formal system that I have been manually translating over to TLA+ . I was debating writing myself a TLA+ generator doing some dumb string-concat logic, but I was curious if there were any tools that would let me pass things into some kind of tree and output TLA+?
--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/65a2da9f-19d4-499d-b233-7377cde1bac1n%40googlegroups.com.
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CALDKJw3FTUaafCD4enKWEkaW3VHiinodAsPjmAK%2Btpv0n%2BOR-w%40mail.gmail.com.
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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAOC8YXZfe%2BoPVDnke-YqYwMy5zmM6p3xHtUqo8HTqVxEDsRshQ%40mail.gmail.com.