Skip to content

JANI to Modest conversion fails for firewire.true from QComp

Using moconv to convert the firewire.true JANI model from QComp to a Modest model creates a property called deadline that collides with the integer variable deadline (bug), and changes the name of variable delay to delay1 (feature). The result is that the toolset can work on the original JANI model, but not on the converted Modest model.

  • JANI model used: firewire.true.v2.jani
  • Modest model produced: firewire.true.3.200.modest
  • Command: modest convert firewire.true.v2.jani -O firewire.true.3.200.modest
  • Modest version: v3.1.238-g896fde292+896fde292c839456e6280620cbd7f2b3aa40f0f5
  • dotnet version: 8.0.104
  • System: Arch Linux 6.8.9-arch1-2