Unfolding with control queries

Bug #1955635 reported by Jiri Srba
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
Fix Committed
Medium
Lena Ernstsen

Bug Description

In the CPN branch, make a timed colored game net with a query
control AF P=1 and press unfold.

It will try to import the query as LTL or CTL, but the unfolding should still be
a timed game net with the
control AF ...
query. It also gives NPE what ever you choose to do.

See also the attached example and press M once you open it.

(use only cpm)

Revision history for this message
Jiri Srba (srba) wrote :
Revision history for this message
Jiri Srba (srba) wrote :

I am still getting this problem - to reproduce:
1. make timed, gamed, CPN
2. make one place P0
3. make a query control AF P0=1, do not verify but only save
4. press M (got to simulator).

Now the premature end of file happens.

Lena Ernstsen (lsaid)
Changed in tapaal:
assignee: nobody → Lena Ernstsen (lsaid)
description: updated
description: updated
Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote (last edit ):

To reproduce:

  - create net net, game + cpn
  - add a new place with one token
  - a new query AF P0 = 1
  - press M
  - select LTL

Error: unfolding failed with error java.lang.StackOverflowError.
Selecting CTL works fine.

Revision history for this message
Kenneth Yrke Jørgensen (yrke) wrote :

I think this is fixed now. However it kind of hacked

Changed in tapaal:
status: New → In Progress
importance: Undecided → Medium
Jiri Srba (srba)
Changed in tapaal:
status: In Progress → Fix Committed
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.