[Bug report] Compiling generated Symbolic Java code FAILED!
Getting this compilation error in the example below using PSym as the target.
The error
[THIS SHOULD NOT HAVE HAPPENED, please report it to the P team or create a GitHub issue]
Compiling generated Symbolic Java code FAILED!
[ERROR] COMPILATION ERROR :
[ERROR] /home/bruno/dev/formal-methods/p_lang_crash_repro_1/PGenerated/Symbolic/SingleDecreePaxosProgram.java:[92,73] incompatible types: psym.valuesummary.PrimitiveVS<java.lang.Integer> cannot be converted to psym.valuesummary.UnionVS
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.1:compile (default-compile) on project SingleDecreePaxos: Compilation failure
[ERROR] /home/bruno/dev/formal-methods/p_lang_crash_repro_1/PGenerated/Symbolic/SingleDecreePaxosProgram.java:[92,73] incompatible types: psym.valuesummary.PrimitiveVS<java.lang.Integer> cannot be converted to psym.valuesummary.UnionVS
[ERROR]
[ERROR] -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoFailureException
Environment
p --version
P version 2.2.2.0
~~ [PTool]: Thanks for using P! ~~
mvn --version
Apache Maven 3.6.3
Maven home: /usr/share/maven
Java version: 11.0.24, vendor: Ubuntu, runtime: /usr/lib/jvm/java-11-openjdk-amd64
Default locale: en_US, platform encoding: UTF-8
OS name: "linux", version: "6.8.0-45-generic", arch: "amd64", family: "unix"
Code to reproduce
// PTst/TestDriver.p
machine Foo {
start state Init {
entry {
var count: map[any, int];
var value: int;
value = 1;
count[value] = count[value] + 1;
}
}
}
// project.pproj
<Project>
<ProjectName>SingleDecreePaxos</ProjectName>
<InputFiles>
<PFile>./PSrc/</PFile>
<PFile>./PSpec/</PFile>
<PFile>./PTst/</PFile>
</InputFiles>
<OutputDir>./PGenerated/</OutputDir>
<Target>PSym</Target>
</Project>
@aman-goel can you please help here?
Hi @PoorlyDefinedBehaviour . Thanks for trying out PSym!
PSym currently does not support type-casting with the any data type.
Try changing var count: map[any, int]; to var count: map[int, int];.
Hi @PoorlyDefinedBehaviour . Thanks for trying out PSym! PSym currently does not support type-casting with the
anydata type. Try changingvar count: map[any, int];tovar count: map[int, int];.
I see, would it make sense to improve the error message a little bit?
We are planning to drop the support for PSym.