Erro QueryVerificationResult in example Model.jar in runtime

46 views
Skip to first unread message

Aristoteles Marçal

unread,
Jan 27, 2020, 10:24:50 PM1/27/20
to UPPAAL
I'm having trouble using the query check (QueryVerificationResult) with the example of model.jar in run-time. Could someone help me?

Code:

     try{
                
                final QueryVerificationResult qvr = engine.query(system, "", "E<> true", new QueryFeedback() {
                    @Override''
                    public void setProgressAvail(final boolean b) {

                    }

                    @Override
                    public void setProgress(final int i, final long l, final long l1, final long l2, final long l3, final long l4, final long l5, final long l6, final long l7, final long l8) {

                    }

                    @Override
                    public void setSystemInfo(final long l, final long l1, final long l2) {

                    }

                    @Override
                    public void setLength(final int i) {

                    }

                    @Override
                    public void setCurrent(final int i) {

                    }

                    @Override
                    public void setTrace(final char c, final String s, final ArrayList<SymbolicTransition> arrayList, final int i, final QueryVerificationResult queryVerificationResult) {
                    }

                    @Override
                    public void setFeedback(final String s) {
                        
                    }

                    @Override
                    public void appendText(final String s) {
                    }

                    @Override
                    public void setResultText(final String s) {
                    }
                });
                final char result = qvr.result;

                // Process the query result
                if (result == 'T') {
                    System.out.println("True");
                } else if (result == 'F') {
                    System.out.println("False");
                } else if (result == 'M') {
                    System.out.println("M");
                } else {
                    System.out.println("Falha");
                }
            } catch (EngineException  | NullPointerException e) {
                // Something went wrong
                System.out.println("Falha na verificacao ...");
            }     



Erro:

Syntax error
        at com.uppaal.engine.Parser.parseProlog(Parser.java:51)
        at com.uppaal.engine.Parser.parseAcknowledgement(Parser.java:426)
        at com.uppaal.engine.DotProtocol.setOptions(DotProtocol.java:276)
        at com.uppaal.engine.EngineStub.setOptions(EngineStub.java:558)
        at com.uppaal.engine.Engine.query(Engine.java:444)
        at ModelSUMO.runModel(ModelSUMO.java:165)
        at ModelSUMO.run(ModelSUMO.java:89)

Marius Mikučionis

unread,
Jan 28, 2020, 2:22:57 AM1/28/20
to Aristoteles Marçal, UPPAAL
2020-01-28, tue, 04:24 Aristoteles Marçal <totem...@gmail.com> wrote:
I'm having trouble using the query check (QueryVerificationResult) with the example of model.jar in run-time. Could someone help me?

The stack trace shows that something went wrong when sending verification options.
Did you set the options before calling engine.query?
There's ModelDemo.java example included in demo -- did it work for you?

Best regards,
Marius
 
--
You received this message because you are subscribed to the Google Groups "UPPAAL" group.
To unsubscribe from this group and stop receiving emails from it, send an email to uppaal+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/uppaal/a09e37af-4dc7-4760-8578-62136f301007%40googlegroups.com.


--
Marius

Aristoteles Marçal

unread,
Jan 28, 2020, 5:45:46 PM1/28/20
to UPPAAL
The example ModelDemo.java worked perfectly, however it does not come with engine.query.

I don't know what verification options would be called.
To unsubscribe from this group and stop receiving emails from it, send an email to upp...@googlegroups.com.


--
Marius

Marius Mikučionis

unread,
Jan 29, 2020, 5:33:56 AM1/29/20
to UPPAAL


On Tuesday, January 28, 2020 at 11:45:46 PM UTC+1, Aristoteles Marçal wrote:
The example ModelDemo.java worked perfectly, however it does not come with engine.query.

What Uppaal are you using?
I just checked 4.0.15 and 4.1.24 and they both have non-empty options parameter to engine.query.

 

I don't know what verification options would be called.

Quoting 4.1.24/demo/ModelDemo.java:

   public static final String options = "order 0\n"
               + "reduction 1\n"
               + "representation 0\n"
               + "trace 0\n"
               + "extrapolation 0\n"
               + "hashsize 27\n"
               + "reuse 1\n"
               + "smcparametric 1\n"
               + "modest 0\n"
               + "statistical 0.01 0.01 0.05 0.05 0.05 0.9 1.1 0.0 0.0 1280.0 0.01";

The options information is available via engine.getOptionsInfo(). 
Note that the result is an XML document describing the options, choices, value ranges and defaults.

Aristoteles Marçal

unread,
Jan 29, 2020, 8:35:35 AM1/29/20
to UPPAAL
I am using version 4.1.19.

I added the options but the error persists.

Do you know any examples you can send?

thankful.

Aristoteles Marçal

unread,
Mar 23, 2020, 6:46:34 PM3/23/20
to UPPAAL

follow the code.

Thank's.


String options = "order 0\n" + 
                    "reduction 1\n" + 
                    "representation 0\n" + 
                    "trace 0\n" + 
                    "extrapolation 0\n" + 
                    "hashsize 27\n" + 
                    "reuse 1\n" + 
                    "smcparametric 1\n" + 
                    "modest 0\n" + 
                    "statistical 0.01 0.01 0.05 0.05 0.05 0.9 1.1 0.0 0.0 1280.0 0.01";
            try{
Em quarta-feira, 29 de janeiro de 2020 07:33:56 UTC-3, Marius Mikučionis escreveu:
Reply all
Reply to author
Forward
0 new messages