pseuco issueshttps://dgit.cs.uni-saarland.de/groups/pseuco/-/issues2024-03-22T12:43:15+01:00https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/issues/97Development build: Trace action computes double traces2024-03-22T12:43:15+01:00Felix FreibergerDevelopment build: Trace action computes double tracesWhen running a development build, opening the trace action sometimes (but not always) causes two traces to be shown because two trace commands are sent to the worker. (This is caused by an effect being invoked twice; the cancellation is ...When running a development build, opening the trace action sometimes (but not always) causes two traces to be shown because two trace commands are sent to the worker. (This is caused by an effect being invoked twice; the cancellation is not triggered because the state is not updated in-between.)
Restarting the trace from the UI works fine.Dominic ZimmerDominic Zimmerhttps://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/9Execution order of global declarations2023-11-06T16:32:01+01:00Felix FreibergerExecution order of global declarationshttps://pseuco.com/#/edit/remote/6dkqvu2x03i9dew5shm6
https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/3
https://dgit.cs.uni-saarland.de/pseuco/pseuco-cpn-compiler/-/issues/4https://pseuco.com/#/edit/remote/6dkqvu2x03i9dew5shm6
https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/3
https://dgit.cs.uni-saarland.de/pseuco/pseuco-cpn-compiler/-/issues/4https://dgit.cs.uni-saarland.de/pseuco/pseuco-cpn-compiler/-/issues/4Execution order of global declarations2023-11-06T16:31:23+01:00Felix FreibergerExecution order of global declarationsThis program can prints 0, but only 2 should be allowed. See also: https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/3This program can prints 0, but only 2 should be allowed. See also: https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/3https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/3Execution order of global declaration2023-11-06T16:32:02+01:00Felix FreibergerExecution order of global declarationThis program can print 1 or 2, but only 2 should be allowed.This program can print 1 or 2, but only 2 should be allowed.https://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/8Inconsistent shadowing behavior in procedure arguments2023-10-23T23:33:18+02:00Yannick SchilloInconsistent shadowing behavior in procedure argumentsWhile shadowing variables seems to be disallowed everywhere else, procedure arguments can shadow everything, including other procedure definitions:
```
int x;
struct S {
int y;
void test(int x, int x, int y, int y) {}
}
mainAgen...While shadowing variables seems to be disallowed everywhere else, procedure arguments can shadow everything, including other procedure definitions:
```
int x;
struct S {
int y;
void test(int x, int x, int y, int y) {}
}
mainAgent {}
```https://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/7Inconsistent implicit cast from bounded channel to handshake channel2023-10-23T23:15:21+02:00Yannick SchilloInconsistent implicit cast from bounded channel to handshake channelA procedure taking a handshake channel (e.g. `intchan`) can be called with a bounded channel (e.g. `intchan10`), but it cannot be assigned directly:
```
void test(intchan ch) {}
mainAgent {
intchan10 ch;
//allowed
test...A procedure taking a handshake channel (e.g. `intchan`) can be called with a bounded channel (e.g. `intchan10`), but it cannot be assigned directly:
```
void test(intchan ch) {}
mainAgent {
intchan10 ch;
//allowed
test(ch);
//disallowed
intchan ch2 = ch;
//disallowed
intchan ch3;
ch3 = ch;
}
```
As a possible workaround, you can use a procedure to "cast" the channel type:
```
intchan cast(intchan ch) {
return ch;
}
mainAgent {
intchan10 ch;
intchan ch2 = cast(ch);
}
```https://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/6ReturnNotExhaustive not thrown in `if` without `else`2023-10-23T23:00:46+02:00Yannick SchilloReturnNotExhaustive not thrown in `if` without `else`The following code type-checks, although nothing is returned if the condition is false:
```
int test(bool b) {
if (b) {
return 1;
}
}
```The following code type-checks, although nothing is returned if the condition is false:
```
int test(bool b) {
if (b) {
return 1;
}
}
```https://dgit.cs.uni-saarland.de/pseuco/pseuco-java-compiler/-/issues/19Type error on array access in method2023-03-23T09:08:59+01:00Felix FreibergerType error on array access in methodConsider this example:
```
mainAgent {
int[2] a = { 42, 1337 };
int tmp = a[0];
a[0] = a[1];
a[1] = tmp;
println(a[1]);
}
void swap(int[2] a) {
int tmp = a[0];
a[0] = a[1];
a[1] = tmp;
}
```
This errors...Consider this example:
```
mainAgent {
int[2] a = { 42, 1337 };
int tmp = a[0];
a[0] = a[1];
a[1] = tmp;
println(a[1]);
}
void swap(int[2] a) {
int tmp = a[0];
a[0] = a[1];
a[1] = tmp;
}
```
This errors in the `swap` method:
```
...\AppData\Local\Temp\pseuCo IDE\include\Main.java:15: Fehler: Inkompatible Typen: int[] kann nicht in int konvertiert werden
int tmp = a[0];
^
...\AppData\Local\Temp\pseuCo IDE\include\Main.java:23: Fehler: Inkompatible Typen: int kann nicht in int[] konvertiert werden
a[1] = tmp;
^
```https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/issues/86React version of Memory Model checker does not show forced values2023-03-10T10:17:32+01:00Felix FreibergerReact version of Memory Model checker does not show forced valuesConsider [this program](https://pseuco.com/#/edit/remote/nht1xyimij2z0vtn6pad) under weak consistency.
Before:
![image](/uploads/94d58cd075ad890d2c36aa028a2d390d/image.png)
After:
![image](/uploads/f092b0c0ed92c2cdeda424d1295252fc/im...Consider [this program](https://pseuco.com/#/edit/remote/nht1xyimij2z0vtn6pad) under weak consistency.
Before:
![image](/uploads/94d58cd075ad890d2c36aa028a2d390d/image.png)
After:
![image](/uploads/f092b0c0ed92c2cdeda424d1295252fc/image.png)
Note the execution we found actually read 0, despite us forcing 42!
This is a display error, as can be seen when changing the program to inspect the value:
![image](/uploads/41c325fca80066f5f213128f7e8c1ea5/image.png)Dominic ZimmerDominic Zimmerhttps://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/issues/75Toast toasts [to a st]ellar UX2022-01-17T12:38:45+01:00Dominic ZimmerToast toasts [to a st]ellar UXAs mentioned in !35 ([here](https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/merge_requests/35#note_7567), and [here](https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/merge_requests/35#note_7568)), w...As mentioned in !35 ([here](https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/merge_requests/35#note_7567), and [here](https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/merge_requests/35#note_7568)), we want to implement a [Toaster](https://dgit.cs.uni-saarland.de/fefrei/hybrid-documents-reader-core/-/blob/main/Toaster.tsx) to give the user some subtle feedback, particularly when downloading CPN/CPPN and LTS exports.
As implementing a top level toaster in the current Angular+React state may cause unforeseen issues, we move this feature request into an issue to be addressed, once AngularJS has successfully been yote.https://dgit.cs.uni-saarland.de/pseuco/m3/-/issues/30More verbose crashes2021-12-06T12:50:21+01:00Dominic ZimmerMore verbose crashesThere are several instances, where one can get the `m3` server to crash or not reply to the user at all. I don't mind the crashes too much — since they are mostly caused by inproper usage — but reporting to the user that something went w...There are several instances, where one can get the `m3` server to crash or not reply to the user at all. I don't mind the crashes too much — since they are mostly caused by inproper usage — but reporting to the user that something went wrong (and what went wrong) seems crucial to me.
My aim with this issue is to polish up 80% of the outstanding problems with about 20% work. I don't mind getting my fingers dirty myself, either. If you have some specific pointers for me, where to poke, I'll be happy to hear @fkosmale! If fixing these issues seems like to much work, I'd be absolutely happy with a wits-end error message saying `The m3 server worker crashed. Are you sure you are running tinyPseuco code?`.
Currently I am observing these issues:
- [ ] asserting writeValueSet to some program initialization throws `writeValueSet` is not supported, though I thought it was...? ![image](/uploads/b3a1e5530c9d625e20c12bf444b49b66/image.png). As a consequence, the UI gets thrown in a very odd state where said assertion can not be interacted with anymore.
- [ ] providing certain illegal tinyPseuco instructions, such as declarations as `string z = "";`, appear to pass the parser, but don't report back to the server, as the Future throws an exception that is not caught. I'd prefer to catch these kinds of exceptions and report to the user that (something, eg.) parsing went wrong.https://dgit.cs.uni-saarland.de/pseuco/pseuco-ide/-/issues/36Weird things happening with indentation using Tab2021-06-08T10:54:53+02:00Tim SchneiderWeird things happening with indentation using TabWhen I try to add something above a line of code in curly brackets and I press <kbd>Tab</kbd> this happens:
![BugReport1](/uploads/6746cd407ff2a87be25dc8f3d158a3be/BugReport1.png) -> ![BugReport2](/uploads/d85b2490f2a756ef6dd9606e681faae...When I try to add something above a line of code in curly brackets and I press <kbd>Tab</kbd> this happens:
![BugReport1](/uploads/6746cd407ff2a87be25dc8f3d158a3be/BugReport1.png) -> ![BugReport2](/uploads/d85b2490f2a756ef6dd9606e681faae2/BugReport2.png)
Cursor is in line 2, column 0 in the first picture and in line3, column 3 after I pressed <kbd>Tab</kbd>
And when I press <kbd>Tab</kbd> when my cursor is in line 3, column 4 this happens: ![image](/uploads/77c80cd6eafde1e0a398283b78942aaa/image.png)
Cursor is now on line 3, column 7 and the i is replaced by a space.
I'm using Version 2.0.4 with Build `#16898` and Commit `95509ae` on Branch `HEAD`
Java Version: `openjdk 14.0.2 2020-07-14`
OS: Linux Mint 20.1https://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/4Add Assertions2022-03-17T12:09:52+01:00Felix FreibergerAdd AssertionsWe should add assertions, to allow model checking of pseuCo programs (e.g. through the bridge to Promela).
- [x] decide on exact syntax and semantics
- [x] add to AST
- [x] extend parser
- add basic support to semantics
- [x] to htt...We should add assertions, to allow model checking of pseuCo programs (e.g. through the bridge to Promela).
- [x] decide on exact syntax and semantics
- [x] add to AST
- [x] extend parser
- add basic support to semantics
- [x] to https://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-compiler
- [ ] to https://dgit.cs.uni-saarland.de/pseuco/pseuco-cpn-compilerFelix FreibergerFelix Freibergerhttps://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/3Variable can initialize itself2023-10-23T22:56:57+02:00Felix FreibergerVariable can initialize itselfThis program typechecks, but it should not, as `i` is undefined: https://pseuco.com/#/edit/remote/utymq85pdp9x46dz8bvfThis program typechecks, but it should not, as `i` is undefined: https://pseuco.com/#/edit/remote/utymq85pdp9x46dz8bvfpascalpascalhttps://dgit.cs.uni-saarland.de/pseuco/pseuco-ccs-interpreter/-/issues/2CCSInput#computeTypes does not check the channel properly2020-06-15T19:28:22+02:00Johannes HostertCCSInput#computeTypes does not check the channel properly`CCSInput#computeTypes` should call `channel.computeTypes` to check whether the channel is well-formed. It however does not do that in the right order, leading to this CCS expression `c(a)?a.0` passing the typecheck but of course failing...`CCSInput#computeTypes` should call `channel.computeTypes` to check whether the channel is well-formed. It however does not do that in the right order, leading to this CCS expression `c(a)?a.0` passing the typecheck but of course failing in the later evaluation.
More specifically, `a` is already added to the environment when `c(a)` is checked even though it should be the other way around.https://dgit.cs.uni-saarland.de/pseuco/pseuco-cpn-compiler/-/issues/2Add testing criteria for termination2020-06-03T14:12:30+02:00Lena BeckerAdd testing criteria for terminationIt would be nice to make use of the new correctness property that states whether the respective pseuCo-program terminates (cf. [commit in pseuCo-tests repo](https://dgit.cs.uni-saarland.de/pseuco/pseuco-tests/-/commit/cf7f71ccb06f785122a...It would be nice to make use of the new correctness property that states whether the respective pseuCo-program terminates (cf. [commit in pseuCo-tests repo](https://dgit.cs.uni-saarland.de/pseuco/pseuco-tests/-/commit/cf7f71ccb06f785122a9446c666fb2706c762a2e)).https://dgit.cs.uni-saarland.de/pseuco/pseuco-lang/-/issues/2Is dynamic condition handling allowed?2019-11-21T15:07:14+01:00Felix FreibergerIs dynamic condition handling allowed?PseuCo, syntactically, allows you to use expressions in `waitForCondition` and `signal`:
```
monitor Test {
condition c1 with (true);
condition c2 with (false);
void do(bool it) {
waitForCondition(it ? c1 : c2);...PseuCo, syntactically, allows you to use expressions in `waitForCondition` and `signal`:
```
monitor Test {
condition c1 with (true);
condition c2 with (false);
void do(bool it) {
waitForCondition(it ? c1 : c2);
signal(!it ? c1 : c2);
}
}
```
Similarly, conditions can be reassigned:
```
monitor Test {
condition c1 with (true);
condition c2 with (false);
void do(bool it) {
c2 = c1;
waitForCondition(c2);
}
}
mainAgent {
Test t;
t.do(true);
println("it");
}
```
I think it's also clear how that should behave. However, neither the CCS-based nor the Petri-net-based compilers support this right now. (Both compilers crash for both programs, except the CCS-based compiler with the second program, which silently ignores the assignment.) I could implement this, but it's somewhat annoying and would blow up the nets. (Background: `waitForCondition` basically is a procedure call for me, and allowing the would require dynamic dispatch of procedure calls.)
Also note that even if we keep allowing this, conditions cannot be sent in channels, passed to procedures, or returned from procedures.
Do we want to allow this (and implement it), or do we want to disallow this (and reject it in the parser)?pascalpascalhttps://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/issues/65Unknown error: Error: Illegal instance value2019-10-05T19:17:01+02:00Felix FreibergerUnknown error: Error: Illegal instance valuehttps://pseuco.com/#/edit/remote/olv38lrj8xvjqzhyzkd2https://pseuco.com/#/edit/remote/olv38lrj8xvjqzhyzkd2pascalpascalhttps://dgit.cs.uni-saarland.de/pseuco/pseuco-java-compiler/-/issues/18Scoping with lock and unlock2019-07-30T20:20:13+02:00Lennard GäherScoping with lock and unlockThe following code does not compile:
```
mainAgent {
lock locky;
lock(locky);
bool tmp;
unlock(locky);
if(tmp) ;
}
```
Error:
```
error: cannot find symbol
{boolean cond = tmp;
^
symbol: ...The following code does not compile:
```
mainAgent {
lock locky;
lock(locky);
bool tmp;
unlock(locky);
if(tmp) ;
}
```
Error:
```
error: cannot find symbol
{boolean cond = tmp;
^
symbol: variable tmp
location: class Main
1 error
```
Version: PseuCoCo-a7b2f25e15f4e9544e84f9d211e10cc4bbcd0890https://dgit.cs.uni-saarland.de/pseuco/concurrent-programming-web/-/issues/60Memory Model: Inconsistent results after reverting assumption2021-01-21T11:10:46+01:00Felix FreibergerMemory Model: Inconsistent results after reverting assumptionLook at this video: ![2019-06-18_15-53-28](/uploads/b3475ffb28021b5dee0c150bda4b7a2c/2019-06-18_15-53-28.mp4)
At the end, I have 3 solutions, add a constraint, remove it again, and then there are only 2 solutions.Look at this video: ![2019-06-18_15-53-28](/uploads/b3475ffb28021b5dee0c150bda4b7a2c/2019-06-18_15-53-28.mp4)
At the end, I have 3 solutions, add a constraint, remove it again, and then there are only 2 solutions.Fabian KosmaleFabian Kosmale