resolving parsing ambiguity for syntactic lists

Question

I am working on parsing promela code using kframework and encountered with ambiguity in the following grammar: (i.e. both Sequence and DeclLst is a syntactic list with separator ;)

Sequence ::= Step ; Sequence
           | Step

Step ::= ...
       | DeclLst

DeclLst ::= OneDecl ; DeclLst
          | OneDecl

When trying to parse the following fragment of code, an ambiguity occurs:

int a;
int b

My parser complains that this code can be parsed as either

1. two Steps each being a OneDecl , or
2. One Step which is itself a DeclLst

Apparently, the core problem is that two syntactic lists (i.e. Sequence and DeclLst) share the same separator ;.

link to PROMELA grammar

I've searched for this kind of ambiguity problems but all I could find was about associativity or operator precedence issues which seemed not quite relevant.

Can anyone enlighten me with how to fix this grammatically? (or even better, with kframework specific solutions)