Nous avons un modèle en alliage destiné à trouver des blocages possibles dans un système. Il est configuré de telle sorte que lorsqu'un contre-exemple est trouvé, cela implique que le système en cours de modélisation peut avoir un blocage, c'est-à-dire une dépendance circulaire entre les nœuds dans le graphique. Le problème est que le modèle visuel du graphique est si compliqué qu'il est presque impossible de trouver le cycle représentant l'impasse. S'il y avait un moyen de mettre en évidence le cycle, ou du moins de mettre en évidence des arcs orientés «vers le haut» plutôt que «vers le bas», cela nous aiderait à mieux visualiser les choses (dans notre modèle, un système sans interblocage a tous les arcs dirigés vers le bas). Existe-t-il un moyen de mettre en évidence ou de tracer sélectivement des nœuds et des arcs qui créent le contre-exemple?Modèle d'alliage - comment afficher le cycle dans la visualisation du graphique?
0
A
Répondre
0
La première chose qui me vient à l'esprit est que quand Alloy montre une instance d'un prédicat, les différents arguments du prédicat peuvent être stylés spécialement. Vous pouvez donc essayer (1) de définir un prédicat qui est l'inverse de votre assertion, c'est-à-dire qui est valide lorsqu'un blocage est présent et qui assigne un rôle aux nœuds du cycle, et (2) définir le style pour afficher ces nœuds dans une couleur ou une forme distincte. Vous pouvez peut-être masquer tout ce qui est et non dans le cycle, ou le griser.
Merci beaucoup pour votre aide. Nous avons implémenté quelque chose dans le sens de ce que vous avez suggéré et il n'affiche que les nœuds du cycle quand Alloy détecte un cycle de blocage. – johnf
Si votre question a reçu une réponse satisfaisante, Stack Overflow suggère que vous acceptiez cette réponse en cochant la case que vous verrez à côté de chaque réponse à une question que vous avez posée. De cette façon, les recherches peuvent distinguer avec succès entre les réponses aux questions sans réponse. –
Merci - J'ai cliqué sur la case "cocher". – johnf