Repository navigation
Similar state names in different classes should be allowed #24
Description
Why
Two different classes can have states that are named the same.
Currently, if two classes have the same state name they need to be changed to not conflict with each other but that does not make a lot of sense. It should be possible to have the same state names in different classes
Example
Currently the following example gives an error:
@StateSet({"uninitialized", "initialized"})
public class SM1 {
@StateRefinement(to="uninitialized(this)")
public SM1() {...}
@StateRefinement(from="uninitialized(this)", to="initialized(this)")
public void initialize() {...}
}
@StateSet({"uninitialized", "initialized"})
public class SM2 {
@StateRefinement(to="uninitialized(this)")
public SM2() {...}
@StateRefinement(from="uninitialized(this)", to="initialized(this)")
public void initialize() {...}
}
class SimpleTest {
public static void main(String[] args) {
SM1 sm1 = new SM1();
SM2 sm2 = new SM2();
sm1.initialize();
sm2.initialize();
}
}The error provided is:
Sort mismatch at argument #1 for function (declare-fun sm2_state1 (test.project.SM2) Int) supplied sort is test.project.SM1
It happens because when translating into SMT each state is matched with their parameters received and the method uninitialized can only be either matched with SM1 or SM2.
Intended behavior
Allow different classes to have the same state names and disambiguate between them when translating to SMT.
The code snippet above should pass the verification without raising errors.
Steps
- Find out here the translation to SMT of these states is happening and include the class as a prefix before converting into SMT.
- Fix the issues and create examples to test the changes.
Activity
alcides commentedon May 3, 2023
Another alternative is to always use qualified names after the parsing. I.e. we can add a processor that just traverses the tree and replaces simple names in states by qualified names (and maybe predicates as well?).
CatarinaGamboa commentedon May 3, 2023
Yes! I think that is one of the possibilities!
Somewhere in the process we are already adding the class name, as in the example it goes from
uninitialize(this)to something likesm2_state1(obj)in the error message. But probably the change has to be done earlier in the process so that the translation into SMT is correct.rfpg1 commentedon May 12, 2023
I was trying to replicate this error to better understand the problem and try to resolve it
Did exactly the same as the example but it didn't gave me any error
Is this still an error?
CatarinaGamboa commentedon May 26, 2023
Hi, sorry for the late reply, the issue still persists.
I created a branch to replicate the issue.
The error will only show if you run the
CommandLineLaucher. Using the VSCode plugin the error will be hidden since it is handled in the code, it also does not crash the program, it only shows the messageSort mismatch at argument #1 for function (declare-fun sm2_state1 (test.project.SM2) Int) supplied sort is test.project.SM1on the terminal.In Eclipse the command line window shows the following:
Let me know if you need any help setting up the environment or in replicating the issue.
[-]Similar state names in different classes should allowed[/-][+]Similar state names in different classes should be allowed[/+]