max_tracelength option is global, not local

[tnelson]

Example:

#lang forge
option problem_type temporal 

one sig Counter {
    var count: one Int
}
pred init { Counter.count = 0}
pred move { Counter.count' = add[Counter.count, 1] }
pred traces {
    init
    always move
}

-- expect to need 2^<bitwidth> states to loop back around and form a lasso
-- 2 Int: -2, ..., 1
-- 3 Int: -4, ..., 3
-- 4 Int: -8, ..., 7
option max_tracelength 10
test expect {
    -- Confirm extension w/o traces pred (confidence test):
    traces_1: {init and move} for 3 Int is sat 
    -- 16 is too many to loop back in 10 states
    unsat_10_4: {traces} for 4 Int is unsat
    -- however, 8 is not too many to loop back in 10 states
    sat_10_3: {traces} for 3 Int is sat
}

-- Adding this should apply to only the _later_ test cases
option max_tracelength 16
test expect {
    -- with 16 states, we have just enough to loop back
    sat_16_4: {traces} for 4 Int is sat
}

Test unsat_10_4 fails in Forge 2.1.0; if you turn on verbose 5 you'll see that the max tracelength sent to Pardinus is 16 for that test. If options apply in-place, I'd expect the trace length there to be 10.

[tnelson]

@bennn Example demonstrating the option-ordering question as promised. This example where the problem arise is temporal-specific, but seems likely to impact other options as well.

[tnelson]

Folllowing up on this, copying contents of a code-dive mail I just sent. This isn't just temporal options; it's an issue with the exec submodule.

Forge option statements are supposed to take effect at their position in the module. So this should pass:

#lang forge
option no_overflow false // default
test expect {
    overflow_allowed: {some i: Int | i > 0 and add[i,1] < 0} is sat
}
option no_overflow true 
test expect {
    overflow_forbidden: {some i: Int | i > 0 and add[i,1] < 0} is unsat
}

Unfortunately, this isn't currently happening. The issue is that, since we shuffle the execution of runs and tests to the end of a module (via the execs submodule) , they're displaced from their context between options. So something that expands as
option = 1
run A
option = 2
run B

will actually run as
option = 1
option = 2
run A
run B

We could fix this by just invoking add-to-execs on option statements. This fixes the example above. I believe this will affect how imports treat options, though: the execs module is meant to prevent importing a model file from actually executing anything that module runs. Predicates, sigs, even "run" names will be preserved, but the actual execution won't be.

So if I make this change, options will be excluded, too. Instead, it's worth investigating what is going wrong with the separation of

• declaring a run
• executing a run
  The declaration shouldn't be delayed. And the declaration SHOULD be capturing the current options.

[tnelson]

This issue is not happening for run, which led to finding the issue. There's a candidate fix on the fix_test_import branch. Risks:

• Need to check other execution-generating constructs to confirm the same issue isn't present there;
• Need to create a test case to confirm proper import semantics for options, runs
• I believe this change will cause test runs (by name) to be imported, where before they were not since the creation of the run itself was deferred to the execs submodule. Need to discuss with @sidprasad to make sure this won't interfere with Toadus. (Not urgent.)

[tnelson]

One other threat that comes up is: should the name of a test in module A be bound in a module importing A?

Why does the run macro in forge/core bind the id, rather than allowing the caller to bind the name, or not, as they wish? Perhaps in tests we ought to be using the functional version.