Segmentation fault at synthesis of VME bus controller

[danilovesky]

Synthesis attempt of VME bus controller results in the following error:

./atacs -otys vme.lpn 
ATACS VERSION 6.0
Logging session in:  atacs.log
Now generating atomic gate implementations.
Using single-cube algorithm for synthesis.
Converting Petri net to ER and storing to:  vme.er
Segmentation fault (core dumped)

Here is the vme.lpn file that was used:

.inputs dsr dsw ldtack
.outputs d dtack lds
#@.init_state [000000]
.graph
d+ dtack+
d+/1 lds+/1
d- p3 p4
d-/1 dtack+/1
dsr+ lds+
dsr- d-
dsw+ d+/1
dsw- p3 p4
dtack+ dsr-
dtack+/1 dsw-
dtack- p1
lds+ ldtack+
lds+/1 ldtack+/1
lds- ldtack-
ldtack+ d+
ldtack+/1 d-/1
ldtack- p2
p1 dsr+ dsw+
p2 lds+ lds+/1
p3 lds-
p4 dtack-
.marking {p1 p2}
.end

[cjmyers]

This works for me. Are you certain that you have write permissions in the directory in which you ran this command?

On Apr 14, 2017, at 11:03 PM, Danil Sokolov notifications@github.com wrote:

Synthesis attempt of VME bus controller results in the following error:

./atacs -otys vme.lpn ATACS VERSION 6.0 Logging session in: atacs.log Now generating atomic gate implementations. Using single-cube algorithm for synthesis. Converting Petri net to ER and storing to: vme.er Segmentation fault (core dumped) Here is the vme.lpn file that was used:

.inputs dsr dsw ldtack .outputs d dtack lds

@.init_state [000000]

.graph d+ dtack+ d+/1 lds+/1 d- p3 p4 d-/1 dtack+/1 dsr+ lds+ dsr- d- dsw+ d+/1 dsw- p3 p4 dtack+ dsr- dtack+/1 dsw- dtack- p1 lds+ ldtack+ lds+/1 ldtack+/1 lds- ldtack- ldtack+ d+ ldtack+/1 d-/1 ldtack- p2 p1 dsr+ dsw+ p2 lds+ lds+/1 p3 lds- p4 dtack- .marking {p1 p2} .end — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/MyersResearchGroup/ATACS/issues/61, or mute the thread https://github.com/notifications/unsubscribe-auth/ADWD91Abl0CkOeTVW9w8qxj5tqCXsEBlks5rv-05gaJpZM4M-IlF.

[danilovesky]

Yes, as a dozen of other LPNs synthesise just fine in the same directory.

If it helps I ran it on Ubuntu 16.04, x86_64.

[cjmyers]

This is not the same as vme.lpn in our examples directory:

.name vme .inputs dsr ldtack .outputs lds d

@.init_state [0000]

.graph dsr+/1 lds+/1 dsr-/1 lds-/1 dsr-/1 d-/1 ldtack+/1 d+/1 ldtack-/1 lds+/1 lds+/1 ldtack+/1 lds-/1 ldtack-/1 d+/1 dsr-/1 d-/1 dsr+/1 .marking {<ldtack-/1,lds+/1><d-/1,dsr+/1>} .end

Where is this one from?

On Apr 15, 2017, at 2:08 PM, Danil Sokolov notifications@github.com wrote:

Yes, as a dozen of other LPNs synthesise just fine in the same directory.

If it helps I ran it on Ubuntu 16.04, x86_64.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MyersResearchGroup/ATACS/issues/61#issuecomment-294292255, or mute the thread https://github.com/notifications/unsubscribe-auth/ADWD99e0k5Xr7q1b1Za-4UnhQQaBrjOqks5rwMFdgaJpZM4M-IlF.

[danilovesky]

The VME spec I tried is exported from a Workcraft model. Note it has both read and write modes. I think it is a "classic" STG from an old Alex's or Jordi's paper.

[cjmyers]

Our parser requires all transitions to have “/#” or none for a given signal. The file you sent fails this requirement. When I fixed the file to meet this requirement, it finds there are 3 CSC violations. Unfortunately, our CSC solver fails to solve this one. It appears to be having trouble inserting the state variable in a consistent fashion.

On Apr 15, 2017, at 2:08 PM, Danil Sokolov notifications@github.com wrote:

Yes, as a dozen of other LPNs synthesise just fine in the same directory.

If it helps I ran it on Ubuntu 16.04, x86_64.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MyersResearchGroup/ATACS/issues/61#issuecomment-294292255, or mute the thread https://github.com/notifications/unsubscribe-auth/ADWD99e0k5Xr7q1b1Za-4UnhQQaBrjOqks5rwMFdgaJpZM4M-IlF.

[danilovesky]

Thank you for explaining this! I will make sure .lpn files passed to ATCS meet this requirement. However it would be nice to produce a meaningful error message at ATACS side if the input file is incorrect (probably a separate issue should be created for this).

[cjmyers]

Agreed.

On Apr 18, 2017, at 9:49 AM, Danil Sokolov notifications@github.com wrote:

Thank you for explaining this! I will make sure .lpn files passed to ATCS meet this requirement. However it would be nice to produce a meaningful error message at ATACS side if the input file is incorrect (probably a separate issue should be created for this).

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MyersResearchGroup/ATACS/issues/61#issuecomment-294850030, or mute the thread https://github.com/notifications/unsubscribe-auth/ADWD965NbAL4eNB76aXCRS4lDBO4MFImks5rxL9XgaJpZM4M-IlF.