Circuit STG has redundant transitions
Bug #1413679 reported by
Danil Sokolov
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| Workcraft |
Fix Committed
|
Medium
|
Danil Sokolov | ||
Bug Description
The STG generated from a circuit may have unnecessary transitions. This is because the gate set/reset functions are not minimised before mapping them into STG.
Consider the attached circuit (it's an implementation of a C-element). In the STG obtained by WC there are 3 out+ and 4 out- transitions (should be one of each). Moreover, some of these transitions are dead due to having both places out=0 and out=1 in their presets.
A correct way for minimisith the STG complexity can be found on page 9 of:
http://
Related branches
lp:~danilovesky/workcraft/trunk-bug-1413679
- Danil Sokolov: Approve
-
Diff: 546 lines (+119/-59)15 files modifiedCircuitPlugin/src/org/workcraft/plugins/circuit/CircuitSettings.java (+23/-0)
CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java (+5/-5)
CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java (+30/-2)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java (+3/-3)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java (+3/-3)
DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java (+4/-4)
MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java (+21/-14)
MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java (+3/-2)
MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java (+5/-5)
MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java (+1/-1)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java (+4/-3)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java (+3/-3)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java (+5/-8)
MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/PunfTask.java (+6/-3)
PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java (+3/-3)
Revision history for this message
| Danil Sokolov (danilovesky) wrote | #1 |
Revision history for this message
| Danil Sokolov (danilovesky) wrote | #2 |
| Changed in workcraft: | |
| status: | Confirmed → Opinion |
| importance: | Medium → Low |
| Changed in workcraft: | |
| status: | Opinion → In Progress |
| importance: | Low → Medium |
| milestone: | none → 3.0.4 |
| Changed in workcraft: | |
| status: | In Progress → Fix Committed |
To post a comment you must log in.
The gate is translated to a circuit Petri net without looking at its context. The read arcs are added at a later stage and in presence of self-loops redundant transitions are possible. I am not sure if this needs to be corrected.