Re: [tlaplus] Is there an approach that allows the TLA+ Toolbox to read the initial state from a predefined text file?

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

You can efficiently serialize and deserialize TLA+ values with the  IO(Des|S)erialize  operators [1] from the CommunityModules.  Less efficient serialization can be done with the help of the Json module [2].

Markus

[1] https://github.com/tlaplus/CommunityModules/blob/f070b68b02cf5b6d085797402374d85f739c167e/modules/IOUtils.tla#L9-L11
[2] https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla

> On Aug 31, 2023, at 9:02 PM, Guo Hua <fchdir@xxxxxxxxx> wrote:
> 
> I have multiple TLA+ specifications with the same initial state space. The initial state space was computed through a lengthy computation and would require a significant amount of time. Is there an approach that allows the TLA+ Toolbox to read the initial state from a predefined text file? This file could potentially be the output of another model checking process, thus saving time. 

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C4114358-DF88-47ED-BE0C-20E8EA7D17B5%40lemmster.de.