hhu-stups / prob-issues

ProB issues (for probcli, ProB Tcl/Tk, ProB2, ProB2UI)
6 stars 0 forks source link

Internal Exception in Trace Replay when SavedAt date in unexpected format #2

Open leuschel opened 3 years ago

leuschel commented 3 years ago

I created a JSON prob2trace file from within ProB Tcl/Tk and tried to replay it. I got:

java.time.format.DateTimeParseException: Text ' 23/12/2020 14:33' could not be parsed at index 0
    at java.base/java.time.format.DateTimeFormatter.parseResolved0(DateTimeFormatter.java:2051)
    at java.base/java.time.format.DateTimeFormatter.parse(DateTimeFormatter.java:1953)
    at com.fatboyindustrial.gsonjavatime.InstantConverter.deserialize(InstantConverter.java:32)
    at com.fatboyindustrial.gsonjavatime.InstantConverter.deserialize(InstantConverter.java:18)
    at com.google.gson.internal.bind.TreeTypeAdapter.read(TreeTypeAdapter.java:69)
    at com.google.gson.internal.bind.ReflectiveTypeAdapterFactory$1.read(ReflectiveTypeAdapterFactory.java:131)
    at com.google.gson.internal.bind.ReflectiveTypeAdapterFactory$Adapter.read(ReflectiveTypeAdapterFactory.java:222)
    at com.google.gson.Gson.fromJson(Gson.java:932)
    at com.google.gson.Gson.fromJson(Gson.java:1003)
    at com.google.gson.Gson.fromJson(Gson.java:975)
    at de.prob.json.JsonManagerRaw.readRaw(JsonManagerRaw.java:79)
    at de.prob.json.JsonManager.read(JsonManager.java:155)
    at de.prob.json.JsonManager.readFromFile(JsonManager.java:290)
    at de.prob.check.tracereplay.TraceLoaderSaver.load(TraceLoaderSaver.java:43)
    at de.prob2.ui.animation.tracereplay.TraceFileHandler.load(TraceFileHandler.java:60)
    at de.prob2.ui.animation.tracereplay.ReplayTrace.getPersistentTrace(ReplayTrace.java:129)
    at de.prob2.ui.animation.tracereplay.TraceChecker.replayTrace(TraceChecker.java:64)
    at de.prob2.ui.animation.tracereplay.TraceChecker.check(TraceChecker.java:57)
Screenshot 2020-12-23 at 14 37 23
leuschel commented 3 years ago

Here is the content of the file:

{
  "description": "File created by ProB Tcl/Tk",
  "transitionList": [
   {
   "name": "$initialise_machine",
   "params": {
     },
   "results": {
     },
   "destState": {
        "active": "{}",
        "ready": "{}",
        "waiting": "{}"
     },
   "destStateNotChanged": [
     ],
   "preds": null
   },
   {
   "name": "new",
   "params": {
        "pp": "PID1"
     },
   "results": {
     },
   "destState": {
        "waiting": "{PID1}"
     },
   "destStateNotChanged": [
        "active",
        "ready"
     ],
   "preds": null
   },
   {
   "name": "new",
   "params": {
        "pp": "PID3"
     },
   "results": {
     },
   "destState": {
        "waiting": "{PID1,PID3}"
     },
   "destStateNotChanged": [
        "active",
        "ready"
     ],
   "preds": null
   }
  ],
 "metadata": {
  "fileType": "Trace",
  "formatVersion": "1",
  "savedAt": " 23/12/2020 14:33",
  "creator": "probtclk",
  "proBCliVersion": "1.10.1-nightly",
  "proBCliRevision": "513fd8b832d9cdc960d82b418a0d8196e241f3d6",
  "modelName": "scheduler",
  "modelFile": "/Users/leuschel/git_root/prob_examples/public_examples/B/Demo/scheduler.mch"
  }
}
leuschel commented 3 years ago

I think it would be nice to have a warning message when the date parsing failed instead of the internal exception and that one can still use the trace file.