sybila / pithya-gui

R based GUI for biodivine

Pithya is a tool for parameter synthesis of ODE-based models and properties based on a hybrid extension of CTL.

Online demo

To try Pithya online, visit pithya.fi.muni.cz. In case of any problems/questions, feel free to contact us at [email protected].

Installation and dependencies

To run Pithya, you need to have Java 8+ and Microsoft Z3 4.5.0 and R installed. If your OS is supported, we strongly recommend downloading precompiled Z3 binaries from github (Pithya allows you to specify a custom Z3 location, so you don't necessarily need to have it in your PATH, but we recommend doing that anyway).

The full installation process for the GUI is described in the manual. You can also use Pithya from command line. For more information, see the core module repository.

Project status

Pithya is composed of several independent modules. Here you can find links to them and their current status:

CTL Model Checker

CTL Query Parser

ODE State Space Generator

pithya-gui's Issues

Editor, run parameter synthesis

Editor.PopUp.ProgressBar.add(run parameter synthesis.click)

Add PopUp Progress Bar on "run parameter synthesis"

=====================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}

Experiment number

When generating approximation or other feature creating new experiment, the current experiment doesn't change. I think it would be more user-friendly if shown experiment would jump into the newest.

Model editor (names and tooltips)

Model editor: Editor

Editor.ProgressBar(accept changes in model.click)
- Syntax of model is good ;) You may proceed with generating abstraction.
+ Syntax of model is without errors ;) You may proceed with generating approximation.
/+ Syntax of model is without errors. You may proceed with generating approximation.

Editor.ProgressBar(generate aproximation.click)
- Abstraction is finished
+ Approximation is generated.

Editor.ProgressBar(reset changes in model.click)
+ Model has been reset.

Editor.ProgressBar(reset changes in properties.click)
+ List of properties has been reset.

Editor.cut thresholds.tooltip
- During The-PWA-approximation of special functions used inside the model new thresholds are generated and some of them could exceed explicit ones. By this checkbox you can tick off this do not be allowed.
+ During The-PWA-approximation of special functions used inside the model new thresholds are generated and some of them could exceed explicit ones. Check to not allow exceeding thresholds.

Editor.Browse.tooltip
- Select input model (with '.bio' extension) for further analysis.
+ Load .bio model file. 

Editor.Property.Browse.tooltip
- Select input model (with '.bio' extension) for further analysis.">
+ Load .bio file for properties.

Editor.Accept changes in model.tooltip
- This button accepts all changes made in editor so they could be passed on to further analysis.
+ Accept all changes in model to continue with analysis.

Editor.Run parameter analysis.tooltip
- "'Model editor' allows the user load, edit or save input model. Simple model is automatically loaded as example."
+ Runs model analysis based on given properties. %TODO

Editor.no/. of threads.tooltip
- "'Model editor' allows the user load, edit or save input model. Simple model is automatically loaded as example."
+ Sets number of threads to compute model exploration with.

Change color of completed upload bar in File loaders

This needs to be done in CSS

Results: Empty states can be selected by double clicking

click inside PS for symbolic parameters doesn't work

should be repaired in next commit

Explorer, approximation of incorrrect model

Approximation of model with syntax error creates experiment:

Editor, parameter value setter

Resize Editor.parameter.box to view whole number.

changes of model, parameter synthesis

Editor.generateApproximation().click -> Editor.runParameterSynthesis().click -> Editor.changeModel() -> Editor.generateApproximation().click

What should tab Results show in this moment?

• old result
• blank
• other

Add default values for plot in model explorer

after clicking on 'add plot' there could be default values - just 1st and 2nd (if possible) values

Unstable sliders

Swift change of value in sliders may cause cycle rewrite.

Explorer, setting values of parameters

When typing value of parameter a bit slow plots start to redraw in cycle.:

Solve:

• set higher delay
  or
• redraw after Enter pressed
  or
• add button parameter to apply value

Model explorer (names and tooltips)

Model explorer: Explorer

Explorer.parameter $name$.tooltip
+ Set parameter value.

Explorer.plot.cancel.name
- cancel
+ delete

Explorer.plot.cancel.tooltip
+ Delete this plot.

Explorer.addPlot.tooltip
- Button will add new layer of plots for vector field or transition-state space or both, depending on which type of input was loaded. 
                                    Then you will be able to play with it.
+ Add new plot for vector field or transition-stace or both.

Explorer.setPlot().horizontal.name
- horizontal
+ horizontal axis

Explorer.setPlot().horizontal.tooltip
+ Set variable to show on horizontal axis.

Explorer.setPlot().vertical.name
- vertical
+ vertical axis

Explorer.setPlot().vertical.tooltip
+ Set variable to show on vertical axis.

< Explorer.length of direction arrows.tooltip>
< - Scaling factor for length of direction arrows inside vector field(s).>
< + Scaling factor for length of direction arrows.>

Explorer.coloring threshold.tooltip
+ Maximal magnitude of vector to be considered neutral (vector with black colour).
/+ Maximal magnitude of neutral vector.

Explorer.plot.hide.click
+ Hide this plot from view.

Explorer.Vector field.use PWA model.tooltip
+ TODO

SetPriority(Maybe)
Explorer.transition-state space of the model.name
- transition-state space of the model
+ state space of the model
SetPriority(previous)

Explorer.Vector field.Unzoom.tooltip
+ Unzoom this vector field plot.
!name dependecy

Explorer.transition-state space.Unzoom.tooltip
+ Unzoom this transition-state space plot.

Explorer.Vector field.Apply to all.tooltip
+ Apply this starting point to all vector field plots.

Explorer.Vector field.Apply to TSS.tooltip
+ Apply this starting point to all vector field plots. (Starting point and axes.)

Explorer.Vector field.Clear plot.tooltip
+ Clear starting point of this plot.

Explorer.Transition-state space.Apply to all.tooltip
+ Apply this starting point to all transition-state space plots. (Starting point and axes.)
!name dependecy

Explorer.Transition-state space.Clear plot.tooltip
+ Clear starting point of this plot.
!name dependecy

Editor, change of model, parameter synthesis

After changes in a model which was already approximated, button "generate approximation" becomes green, which is nice, but button "run parameter synthesis" should become grey and unclickable also.

unzooming problem in PS

when you zoom in PS plot and then you choose another formula its unzoom button will shade (as disabled) even though such plot is zoomed

Results, Selecting same parameter for axes y,y

Results.plot(1).setHorizontal(y) ->Results.plot(1).setVertical(y)
results in
Error: Some duplicate ....
and then both plots (PD and SS) disappear (Fig. 1)

Then Flow:
-> Results.addplot() -> Results.plot(1).setHorizontal(x)

Problem 2:
the plot 1 doesn't set horizontal to x and stay hidden (Fig. 2)

As you can see in the image, I have selected 3 plots but only 1 is visualised

Comment:
without adding second plot, the feature seems working

Explorer, add Default Plot

Explorer.Default.addPlot(Choose,Choose)
Add deafult plot with unset axes (Choose for both)

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}

parameter-variable combination plot problem

all layers react now on any selected state in SSS plot, but it should react only on selected states in the same layer so you could investigate dependence of parameter and variable values

Results, Selecting same parameter for axes deg_x,deg_x

Results.plot(1).setHorizontal(deg_x) ->Results.plot(1).setVertical(deg_x)

The shown plot for parameter space (or parameter dependence) is only 1-dimensional. (Fig. 1)

Problem:
The result is not intuitive

Solve:

• Anable choosing vertical axis as "None" for such 1-dimensional plot
  or
• explicitly warn user that the plot is 1-dimensional
  or
• really show 2-dimensional plot for deg_x vs. deg_x

Missing functionalities

Explorer.transition-stace space.Clear plot
Missing functionality

Explorer.activate/!.click
Missing functionality

Result.activate/!.click
Missing functionality

Explorer.vector field.Unzoom.click
Missing functionality (or runs long without shading plot)
! Explorer.vector field.Unzoom.doubleclick works

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}

naming pictures (UX)

Could we name pictures shown in pythia gui by file name instead of download

move Advanced settings checkbox under the red horizontal line

Explorer, Selecting same parameter for axes

Explorer.plot(1).setHorizontal(y) ->Explorer.plot(1).setVertical(y)
results in:
Error:non-numeric argument to mathematical function

Solve:

• Please write explicitly to choose different parameters in the Error
  or
• Do not draw such plot at all

Result - Browse (UX)

Loading this file from tSCC analysis
model_2D_1P_10kR.txt
was somehow very slow, transition-state space showed almost immediately, but for VF it took few seconds with no loading box or anything.

Explorer, drawing no plot

Flow: Explorer.addPlot(x,y) -> Explorer.deletePlot((x,y))
result: "transition-state space is drown"
drawing progress on deleting last plot

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}
"Flow" Serie of action in GUI (symbol "->" means using with sufficient delay and symbol "|" means without delay(for example doubleclick))

Editor, run parameter synthesis

On offline version:

Generate approximation -> Run parameter synthesis

results in error:
Warning: running command '"..//biodivine-ctl//bin//ode_model" ..//Temp//config.689626.json > ..//Temp//result.689626.json 2> ..//Temp//progress.689626.txt' had status 127

Result plot labels

resuolt plots have wrong labels

Result, changing formula

Flow: DefaultFlow -> Result.choose formula.(bistability?) -> Result.addPlot(deg_x,y)-> Result.choose formula.(high?)
parameter-variable dependecy diagram results in:"Error:Join results in 720 rows; more than 126 = nrow(x)+nrow(i). Check for duplicate key values in i each of which join to the same group in x over and over again. If that's ok, try by=.EACHI to run j for each group to avoid the large allocation. If you are sure you wish to proceed, rerun with allow.cartesian=TRUE. Otherwise, please search for this error message in the FAQ, Wiki, Stack Overflow and datatable-help for advice."

Flow: DefaultFlow -> Result.choose formula.(bistability?) -> Result.addPlot(deg_x,y)-> Result.choose formula.(low?)
parameter-variable dependecy diagram results in:"Error:Join results in 980 rows; more than 147 = nrow(x)+nrow(i). Check for duplicate key values in i each of which join to the same group in x over and over again. If that's ok, try by=.EACHI to run j for each group to avoid the large allocation. If you are sure you wish to proceed, rerun with allow.cartesian=TRUE. Otherwise, please search for this error message in the FAQ, Wiki, Stack Overflow and datatable-help for advice."

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}
"Flow" Serie of action in GUI (symbol "->" means using with sufficient delay and symbol "|" means without delay(for example doubleclick))

Save function

Save function doesn't work:

• Editor.saveModel
• Editor.saveProperties
• Result.saveResults

wrong PS (with clicked point) after switch experiment and switch back

if it is clicked inside PS and experiment is changed and then switched back shown PS is not the same (just visually - data are good) until it is zoomed and unzoomed

Disable zoom button / select button when plot is not zoomed/selected

Prevent very intensive computations (or allow to stop them)

Currently, rendering of big graphs or computing non trivial data (like transitions) cannot be interrupted by the user. So by uploading a very large model, you can overload the server without the ability to recover.

Possible solutions:

• Have an upper bound on model complexity and refuse models which are too big.
• Make such operations interruptible and terminate them when the session ends

Editor, stop parameter synthesis (Windows)

"Stop parameter synthesis" doesn't work on windows.

Editor, no. of threads

Editor.no/. of threads.changelocation(advanced settings)
(move <no/. of threads> to advanced settings )
OR
(remove this function and set maxi no. of threads)

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}

Running Server.R on a new instalation

Warning in file(con, "r") :
cannot open file 'Temp//result.282246.json': No such file or directory

Problem with no such folder Temp

Add logo with external link to sybila page

Editor, reload model

Editor.BrowseModel(xyz) -> Editor.model.change -> Editor.BrowseModel(xyz)

After blanking or editing model, user can't load same model. So you actually can't reload model without loading other model in the process.

Result, save button

Missing Functionality:
Result.save

SS plot for 3 a more variables doesn't work

problem with n-dimensional layers

Explorer, number of parameters

After some changes in parameters in the model I managed to get this error, showing nuber of parameter in Explorer didn't change according to the model.

Explorer, trajectory on zoomed plot

Explorer.SS.plot(1).zoom -> Explorer.VF.plot(1).doubleclick (to view trajectory)

Problem:
Trajectory is not drawn in SS plot

Problem 2:
Not shown even after unzooming the SS plot.

Reset projection checkboxes when advanced mode is disabled

Deletion of last experiment

Currently, the very last experiment (either model or result) generated or loaded as the last one is not possible delete, so user has still something to work with. It is possible to change it, but there will be an issue with latest loaded result file as it can not be reloaded before selecting of other one and then to select back the right one (because of reactive system).

parameter synthesis process problem

on Win parameter synthesis doesn't stop

branch:merging..... ,results.plot views

Flow:
NormalFlow -> Results.addplot.click -> Results.addplot.click -> Results.plot(2).horizontal.set(x) -> Results.VF.plot(2).scaleIn(0.8) | Results.VF.plot(2).scaleIn(0.6)

Results in cycle of changes

Editor; generating approximation, tresholds

In default model
Editor.generateApproximation().click -> Editor.model.diff("THRES: y: 0,4,8, 15","THRES: y: 0,4,5,8, 15") -> Editor.generateApproximation().click ->Editor.properties.diff("low = y < 4","low = y < 5") -> Editor.runParameterSynthesis().click

results in error:
Missing threshold

Status Bar:

Started processing formula y < 5.0
java.lang.IllegalArgumentException: You have to use an exact threshold in propositions! Proposition: y < 5.0, Thresholds: Variable(name=y, range=(0.0, 15.0), thresholds=[0.0, 2.010804, 2.917167, 3.685474, 4.0, 5.564226, 6.290516, 7.082833, 8.0, 8.04922, 9.345738, 11.320528, 15.0], varPoints=null, equation=[1.0*Param(-1)Approx(0)[0.0, 2.010804, 2.917167, 3.685474, 5.564226, 6.290516, 7.082833, 8.04922, 9.345738, 11.320528, 15.0]{1.0, 0.98959, 0.936679, 0.821302, 0.369445, 0.24085, 0.149163, 0.084657, 0.041991, 0.01653, 0.004098}, -1.0Param(1)Var(1)])
at com.github.sybila.ode.generator.AbstractOdeFragment.validNodes(AbstractOdeFragment.kt:49)
at com.github.sybila.checker.ModelChecker.validNodes(ModelChecker.kt)
at com.github.sybila.checker.ModelChecker.verify(ModelChecker.kt:49)
at com.github.sybila.checker.ModelChecker.checkExistUntil(ModelChecker.kt:96)
at com.github.sybila.checker.ModelChecker.verify(ModelChecker.kt:56)
at com.github.sybila.biodivine.exe.MainKt.main(Main.kt:91)
You have to use an exact threshold in propositions! Proposition: y < 5.0, Thresholds: Variable(name=y, range=(0.0, 15.0), thresholds=[0.0, 2.010804, 2.917167, 3.685474, 4.0, 5.564226, 6.290516, 7.082833, 8.0, 8.04922, 9.345738, 11.320528, 15.0], varPoints=null, equation=[1.0Param(-1)Approx(0)[0.0, 2.010804, 2.917167, 3.685474, 5.564226, 6.290516, 7.082833, 8.04922, 9.345738, 11.320528, 15.0]{1.0, 0.98959, 0.936679, 0.821302, 0.369445, 0.24085, 0.149163, 0.084657, 0.041991, 0.01653, 0.004098}, -1.0Param(1)*Var(1)]) (java.lang.IllegalArgumentException)

but
Editor.model.diff("THRES: y: 0,4,8, 15","THRES: y: 0,4,5,8, 15") -> Editor.generateApproximation().click ->Editor.properties.diff("low = y < 4","low = y < 5") -> Editor.runParameterSynthesis().click
works fine

Explorer, not deleting plots

Explorer.plot.cancel / Explorer.Vector field.plot
result: Explorer.plot.cancel does not delete plot, problem with cash, plot saving or smth
After adding deleted plot, programme shows some plot with trajectory in Vector field (not default plot without trajectory)

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}

Explorer, parameter value

Explorer.parameter(deg_x).up | Explorer.parameter(deg_x).up

When increasing value of parameter rapidly, gui results in cycle of changes

Dependent parameters

MODEL:

VARS: x,y
CONSTS: k1,1; k2,1
PARAMS: deg_x,0,1; deg_y,0,1

EQ: x = k1*hillm(y,5,5,1,0) - deg_x*x - deg_y*y
EQ: y = k2*hillm(x,5,5,1,0) 

VAR_POINTS: x: 2500, 10; y: 2500, 10

THRES: x: 0, 15
THRES: y: 0,4,8, 15

Editor.generateApproximation -> Editor.runParameterSynthesis
results in Crash:

Warning in as.data.table.list(x) :
Item 2 is of size 0 but maximum size is 1, therefore recycled with 'NA'
Warning in as.data.table.list(x) :
Item 2 is of size 0 but maximum size is 1, therefore recycled with 'NA'
Warning in as.data.table.list(x) :
Item 2 is of size 0 but maximum size is 1, therefore recycled with 'NA'
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
43: rbindlist
42: reactive:loading_ps_file [E:\BioDivine\biodivineGUI/server.R#1870]
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3317]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3334]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3348]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3381]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3399]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3500]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#1996]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3517]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3531]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3568]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#3580]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2010]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: loading_ps_file
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2021]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
45:
44: stop
43: loading_ps_file
42: reactive:visible_ps_plots [E:\BioDivine\biodivineGUI/server.R#2081]
31: visible_ps_plots
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2302]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: visible_ps_plots
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2324]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: visible_ps_plots
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2347]
1: runApp
Warning: Error in rbindlist: Item 3 has 1 columns, inconsistent with item 1 which has 2 columns. If instead you need to fill missing columns, use set argument 'fill' to TRUE.
Stack trace (innermost first):
33:
32: stop
31: visible_ps_plots
30: observerFunc [E:\BioDivine\biodivineGUI/server.R#2359]
1: runApp
ERROR: [on_request_read] connection reset by peer

Explorer, set axes

Flow: Explorer.plot(1).setHorizontal(#) | Explorer.plot(1).setVertical(#)
result: vertical axis not set
add GUI delay on setting plot axis value

======================================================
LEGEND:
ModulesDict:= {Model editor:Editor,Model explorer:Explorer,Result explorer:Result}
"Flow" Serie of action in GUI (symbol "->" means using with sufficient delay and symbol "|" means without delay(for example doubleclick))