tlaplus/tlaplus

Using `-dump` option to produce state dumps in machine readable format

Open

#1 216 ouverte le 24 juil. 2025

Voir sur GitHub
 (2 commentaires) (0 réactions) (0 assignés)Java (179 forks)batch import
Toolsenhancementhelp wanted

Métriques du dépôt

Stars
 (2 153 stars)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

Description

Recently we touched the topic of model based testing and -simulate configuration of tlc in the TLA+ community.

When using -simulate and -dump options to generate random behaviors of the model with the goal of using them to produce tests for systems written in other languages the question of state dumps parsing arises.

Currently -dump option generates state dumps in TLA+ format. Still, it's quite beneficial to have a machine readable format of such dumps as eventually it will be parsed by the abstract test generator.

Therefore, it's proposed to update the following part of the TLC code so that it generates dumps in JSON format: https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java#L735

Guide contributeur

Direction de recherche
Cette demande propose de modifier l'option ` dump` dans TLC pour produire des dumps d'état au format JSON plutôt qu'au format TLA+. Le fichier clé à modifier est `tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java`, en particulier autour de la ligne 735 où les dumps d'état sont actuellement générés. Une bibliothèque JSON pour Java (par exemple, Jackson ou Gson) doit être utilisée pour sérialiser l'état en JSON. L'implémentation doit garantir que la sortie JSON soit compatible avec les outils d'analyse existants pour la génération de tests, et pourrait nécessiter de mettre à jour l'option ` dump` pour accepter un argument de format ou d'ajouter une nouvelle option.
Stack technique
java
Domaine
tooling
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
JavaGit
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
70