Enable the use PNML versions of Punf and MPSat tools
Bug #1366078 reported by
Danil Sokolov
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| Workcraft |
Fix Committed
|
Low
|
Danil Sokolov | ||
Bug Description
New versions of Punf and MPSat tools support PNML format for unfolding that enables better verification of the models.
However, there are some limitations to these tools:
* PUNF can only generate unfolding prefixes for low-level nets and STGs (no high-level nets, merged processes, LTL-X model checking).
* MPSAT supports deadlock checking, REACH and, perhaps, CSC/USC checking and complex-
Temporary both the old and new versions of the tools need to be supported, the later in experimental mode.
Related branches
lp://staging/~danilovesky/workcraft/trunk-bug-1366078
- Danil Sokolov: Approve
-
Diff: 743 lines (+147/-109)13 files modifiedCircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java (+11/-11)
CpogsPlugin/src/org/workcraft/plugins/cpog/tasks/ProgrammerChainTask.java (+2/-27)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java (+6/-6)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java (+6/-6)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java (+8/-8)
MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java (+32/-1)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java (+12/-8)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java (+14/-9)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/PunfTask.java (+12/-7)
MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java (+17/-8)
MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java (+17/-11)
MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java (+4/-1)
PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java (+6/-6)
| Changed in workcraft: | |
| status: | In Progress → Fix Committed |
To post a comment you must log in.
