[ARTEFACT] Sketchbook: Logical Model Inference from Boolean Network Sketches

Sketchbook Manual Contents 1 Running Sketchbook 3 2Sketchbook Workflow 4 3 Sketch Editor Session 5 3.1 Generalnavigation.................................... 5 3.2 Editingregulatorynetwork ............................... 5 3.2.1 Noteoninputs .................................. 8 3.3 Editingupdatefunctions................................. 9 3.4 Loading and editing datasets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.5 Editingproperties .................................... 11 3.6 Displaying annotations list . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.7 Starting analysis and checking consistency . . . . . . . . . . . . . . . . . . . . . . . 15 4 Inference Session 17 5 Tutorial 20 6 Sketch Format 25 6.1 Logical expressions and languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.1.1 Syntax of update functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.1.2 Syntax of generic dynamic properties . . . . . . . . . . . . . . . . . . . . . . 25 6.1.3 Syntax of generic static properties . . . . . . . . . . . . . . . . . . . . . . . 27 6.2 Datasets.......................................... 27 6.3 Sketchformats ...................................... 27 6.3.1 CustomJSONformat .............................. 27 6.3.2 ExtendedAEONformat............................. 28 6.3.3 SBMLformat................................... 28 1 Intro to Sketchbook Sketchbook is a tool for inference of Boolean networks (BNs) using the logic-based framework of BN sketches [3]. BN sketch provides a formal model specification that integrates diverse types of prior knowledge and experimental data, enabling the application of inference algorithms to identify all admissible BNs. Particularly, a BN sketch consists of an influence graph, a partially specified Boolean network (PSBN), and sets of required structural and dynamic properties that the model must satisfy. Specifically, Sketchbook is a multiplatform desktop application that offers a graphical interface for both editing all components of the BN sketch and running the inference process. Sketchbook consists of two main sessions (or windows): The interactive editor session and an inference session, as illustrated by the workflow below. General workflow of Sketchbook. In the editor window, you can create and validate the model specification (i.e., design the Boolean network sketch) by editing the influence network, PSBNs, datasets with observations, and creating various kinds of static and dynamic properties. Once you have created the specification, you can start the inference window. There, you can then run the inference algorithms and explore or export the set of admissible BNs that satisfy all the properties. This manual covers the following: •We give short instructions on the setup of Sketchbook in Section 1. •The overall workflow of the tool is shortly introduced in Section 2. •We describe the Editor Session of the tool and its features in detail in Section 3. •The Inference Session and results are described in detail in Section 4. •A brief tutorial showcasing the main functionality on a simple model is presented in Section 5. •Supported formats for datasets, sketches, and syntax for various kinds of supported expressions are discussed in Section 6. 2 1 Running Sketchbook This section provides general instructions for installing and setting up Sketchbook. The tool’s repository with the latest version of the source code (that is licensed under the MIT license) is freely available at our GitHub: https://github.com/sybila/biodivine-sketchbook. We provide pre-built binaries and installation files for the application in the release section of the repository. To start using Sketchbook, choose the latest release and download a binary for your operating system. You choose between .app and .dmg for macOS,.AppImage,.deb and .rpm for Linux, or .exe and .msi for Windows. If you need a different pre-built binary for a specific platform, let us know! Note that on newer Linux distributions (Ubuntu 24 or Debian 13), some Tauri dependencies may not be supported by default. This does not affect the setup through the .AppImage (as it bundles all dependencies inside). However, it may affect installation with the .deb package, where you need to first install libwebkit2gtk-4.0. See a solution for that at this GitHub issue. This will be resolved once we switch to Tauri 2. When installing the binaries, note that they are not signed with official developer certificates, so macOS and Windows will most likely require you to grant special permissions to run the app. On newer versions of macOS, the message is that the app is corrupted. This is still the same issue regarding app certificates. You should be able to “enable” the app by running xattr -c /path/to/biodivine_sketchbook.app. Alternatively, the desktop application can also be built directly from the repository’s source code. To do this, please consult the Development guide of the repository Readme. Note that the local build requires additional dependencies to be installed. After successfully starting the application, you should see the following screen: Initial screen of Sketchbook. 3 2Sketchbook Workflow As discussed in the introduction, Sketchbook operates through two main sessions: the Editor Session, where you create and validate the model specification (i.e., design the Boolean network sketch), and the Inference Session, where you compute and explore all network candidates consistent with the specification. Each session operates independently, maintaining its own lifecycle and internal state. The main workflow proceeds as follows, with details on both sessions provided in the subsequent sections. First, you design the influence network by defining variables and their regulatory interactions in the Network tab (see Section 3.2). Each regulation can be annotated with its monotonicity (activation, inhibition, dual, or unknown) and essentiality (essential, non-essential, or unknown). Next, you can assign each variable a partially specified update function in the Functions tab (Section 3.3). These can be standard logical expressions, but may also involve supplementary uninterpreted functions representing unknown parts of the update mechanism to be determined by the inference. You can specify additional properties of these partially specified functions in the Properties tab, as discussed below. You may import and edit binarised experimental datasets in the Observations tab (Section 3.4). The observations may come from steady-state or time-series expression measurements. These observations are later incorporated into dynamic properties (such as fixed points or trajectories) to constrain model behaviour in the Properties tab, as discussed below. Then, you can define various required model properties in the Properties tab (Section 3.5). Static properties restrict the structure of the model (constraints on admissible update functions), while dynamic properties capture expected model behaviour. Dynamic properties can directly incorporate datasets, for example, to link observations to fixed points, attractors, trap spaces, or trajectories. You can either use predefined property templates or specify the properties directly as logical formulas. Before running inference, you can run a static validation check on the overall consistency of the sketch in the Analysis tab (Section 3.7). Detected issues can be reviewed and corrected directly in the editor. Finally, once you finish editing the specification, start the Inference Session (Section 4) from the Analysis tab. A new window appears, where you can run the computation. The tool will compute all Boolean network models consistent with the specified sketch at once. Once inference finishes, you can review the summary of results (e.g., the summary of admissible functions), sample admissible networks, or export the compact symbolic encoding of the results for further analysis and refinement. Note that once an Inference Session starts, any changes made in the editor afterwards will not affect that session. Each session works with a fixed snapshot of the model and its settings taken at the time it was created. You can, however, create multiple inference sessions simultaneously, each with its own inputs or configurations. 4 3 Sketch Editor Session The sketch editor is the primary session of the tool that allows editing all components of the sketch. The tool starts with a simple initial screen where you can select the first action. This can be loading a sketch in various formats, creating a new empty sketch, or choosing a prepared example. Choose one of the buttons and continue: Available buttons at the initial screen. The following subsections then summarize the options available in the editor. 3.1 General navigation At the top of the screen, there is a pop-up menu, a list of tabs, and an undo-redo button. Navigation bar at the top of the screen. Each tab offers different functionality, as discussed below. You can select any of them by clicking on the tab button. Tabs can also be "locked," allowing two tabs to be displayed side by side. To do so, click on the small “lock button” at the bottom left of the screen. The menu offers options regarding import/export. You can import sketches in JSON, AEON, or SBML format, and we also support exporting the sketch in JSON and AEON. You can also export the network image as a PNG. More details on the formats are in Section 6. Note that importing a new sketch results in losing current data (you’ll get a warning). Menu with all the options. Lastly, you can use the undo and redo buttons in the top right corner to reset or reapply your last actions. 3.2 Editing regulatory network The editor starts with the Network tab opened. If a new project is started, a help message is displayed. The message disappears after you start editing the network, but you can reopen it by hovering over the “question mark” button in the lower-right corner of the screen. The user can then edit or load the network. 5 Empty network tab of the editor session with a help message. A new variable can be added by double-clicking in the free space. You can drag variables to achieve any kind of layout. Then, you can select a variable (by clicking on it) to get a context menu with options to add regulations, edit the variable, or edit its update function. Variable context menu. Regulation context menu. Regulation can be added by clicking the corresponding “+” button and dragging the arrow that appears towards another variable. The option for editing a variable opens a dialogue window where you can edit its name, ID, and annotation. 6 Example of a dialogue window to edit a variable. You can also select a regulation and customize it. We offer customizing two kinds of regulatory properties – monotonicity and observability. Monotonicity allows us to specify what type of effect the interaction has. The monotonicity of the regulation is reflected by its colour. The options are: •activation for positive monotonicity (green colour) •inhibition for negative monotonicity (red colour) •dual for non-monotonous effect (blue colour) •unknown for undefined (grey color) Essentiality allows us to specify whether the regulation must always have an effect on its target, or whether it may be “redundant”. Essentiality is reflected by different line styles. The options are: •essential for regulations that must always have an effect (solid line) •unknown regulations that may or may not have an effect (dashed line) •non-essential for regulation being completely redundant (dotted line) The fully edited network can look like the following: 7 Network tab with an example of a created regulation network. 3.2.1 Note on inputs When creating input nodes, if you leave the node without regulation, it can only take a single fixed value in any interpretation. To allow the node to be fixed to either value within the same interpretation, you can add an essential self-activation. For convenience, nodes with no incoming regulations are highlighted in blue, and a tooltip about input modelling is shown when you hover over them. Illustration of two variants of input modeling, including the tooltip hint. 8 3.3 Editing update functions Logical update rules and supplementary functions can be edited within the Functions tab. On the left side of the screen, you can see a list of variables, their regulators and their update functions. On the right side, you can create additional supplementary functions that can be used inside the update function expressions. Functions tab with partially specified update functions for three variables and three supplementary functions. For each variable, you can edit the type of regulations by clicking on the monotonicity or essentiality value. This is propagated to the network tab. You can also edit the update function’s expression. The format of update functions is discussed in Section 6.1.1. List of regulators and update expression for variable v3. You can add new supplementary functions at the top bar by clicking the +ADD button. You must always add a new supplementary function before using it in any expressions. For each function, you can increment or decrement its arity, update monotonicity/essentiality properties, set its partial expression, edit its details (same as for a variable, via an external dialogue), or delete it. The details of a supplementary function can be hidden by collapsing it. 9 shown an error message. However, there can still be some inconsistencies in the sketch – property templates with some fields not filled, logical formulas referencing non-existent variables, and so on. To check the consistency of the sketch, click on the RUN CONSISTENCY CHECK. An exhaustive static check is run on the sketch, reporting all issues in the text area under the consistency check button. If some minor non-critical issues are encountered (such as if a dataset is defined but not utilised in any dynamic properties), a simple warning message will pop up. Users can decide whether it is relevant and whether they should address it or not. Analysis tab with a sketch summary, a button to start the inference window, and a button to run a consistency check. An example of detected inconsistencies is shown in the text window. Example of a consistency warning. Finally, after clicking on the START INFERENCE SESSION, a new window opens. We go into detail on the inference session functionality in Section 4. You can open multiple inference sessions at the same time. After opening a new session, it uses the version of the sketch at the time of its creation. Subsequent changes made in the editor do not affect any already running inference. 16 4 Inference Session After starting the new inference session, a simple window appears where you can run the inference. You can choose from two options: running the full inference with all properties or performing a preliminary step – a partial “static” inference with static properties only. The static properties are usually much faster to evaluate. You can check the results, and if the candidate set is too large, you might first want to add more static properties, before running the full inference. Inital inference screen with the options to run two variants of inference. Once you click one of the buttons to run the inference, the backend starts the computation. You’ll see the progress summary and a report. In the report, you’ll see various checkpoints reached during the computation, such as when all inputs are processed or when a property is evaluated. For each such checkpoint, the time of reaching it and the number of remaining consistent candidates are reported. At any point, you can cancel and restart the computation by clicking the START AGAIN button. In the background, the ongoing computation completes its current task (such as evaluating a single property) and gets terminated. An example of the intermediate progress output during computation. Once the computation finishes, you’ll see a screen with a summary of results, a progress report, and options to export the results or sample admissible BNs. 17 Inference window with a summary and buttons to export/sample the results. Summary and report The summary includes the number of admissible candidates at various stages of the algorithm, computation times, and the number of admissible update functions per variable. The summary of admissible update functions can help to identify which parts of the model are consistent across candidates and which are more variable, enabling refining the sketch accordingly. For example, if you see that there is only one option for an update function possible for a given variable, you can automatically refine your sketch before running subsequent computations. Export of results You can export the full results (by clicking the SAVE FULL RESULTS) button. After you choose the path, the results are exported in an archive that contains the following components: •A serialized BDD encoding all the admissible BN interpretations. The BDD format is compatible with the format used by the aeon.py library [1]. •Original sketch used as an input for the inference. This is included for replicability. •Derived parametrized aeon model used internally during the computation. This model gives context to the BDD variables. •Computation report encompassing all the information shown in the UI. •Folder with a list of admissible update function variants per each variable. 18 Results archive structure. Sampling admissible networks Finally, you can randomly sample the fully specified admissible candidate networks (as .aeon files). To generate witness networks, click on the SAMPLE NETWORK(S) button. You can select how many witnesses to generate and also select a random sampling (the default sampling is deterministic). By clicking the button, a file save dialogue will open. Witness files are saved in a .zip archive. Example of a sampling dialogue. 19 5 Tutorial To illustrate the main workflow and functionality of Sketchbook, we use a toy version of the FGF signalling network, inspired by the model introduced in [4]. Note that the model is intentionally simplified and serves only to illustrate the main features of the tool. Most of the regulations are mediated by other entities or whole cascades in the real system. We also do not go into unnecessary details regarding the tool’s interface (such as various buttons or options), as the functionality is introduced in previous sections. We start by creating the following influence graph in the Network Editor. It contains 5 variables: FGFR_stim,FGFR3,FRS2,ERK, and RAS. The FGFR_stim is modelled as an input node that activates the FGFR3 receptor. The input has a single self-activating regulation to ensure it does not change value. This way, we also ensure that both values of the input are possible in all model interpretations. The FGFR3 can then activate ERK either through FRS2 or RAS (both representing whole activation cascades). There is a negative feedback from FRS2 back to FGFR3 (mediated by GRB2 in the original model) and from ERK back to FRS2 (mediated by SPRY in the original model). Next, we assign the partial update functions (considering prior knowledge). For the variables FGFR_stim and RAS, there is only one way to set up the functions, so we fill them directly. Next, suppose that FGFR3 requires both the presence of FGFR_stim and the absence of FRS2. Lastly, let’s assume the particular update rules of ERK and FRS2 are unknown and to be determined by the inference. We can assign them binary function symbols for now, and the inference process will find satisfying interpretations of these functions. Together, we get the following PSBN: FFGFR_stim =FGFR_stim FFGFR3 =FGFR_stim ∧ ¬FRS2 FRAS =FGFR3 FERK =f(RAS,FRS2) FFRS2 =g(FGFR3,ERK) We can specify this PSBN in the Function Editor. First, we have to add the two supplementary functions fand g, both with arity 2 (and we do not select any of their properties). 20 We can then set all the update functions as described above: Next, let’s prepare some dynamic properties utilising simple observations. We will only consider measurements of ERK for this simple case (values of other variables can be left unspecified). First, it was measured that in the long term, ERK can stabilise in both active and inactive states. This gives us two observations, and we will use them to define model fixed points in the next step. Furthermore, suppose we did simple time series measurements with ERK and observed that starting with the inactive form, it becomes active and then goes back to inactive. This gives us three transient observations that we will use to define a trajectory property of the model in the next step. We can specify the measurements in the Observations Editor. Specifically, we create two datasets, one with steady state observations and one for the transient time series. 21 Then, in the Properties Editor, we link the observations to the corresponding required dynamic properties. We create two Fixed points properties for the two steady-state observations, and a Trajectory property to capture the transient ERK pulse. Furthermore, Sketchbook automatically creates static properties encoding monotonicity and essentiality of the regulations (reflecting the Network Editor). Some of these are illustrated below. In this example, we do not add any additional static properties. With that, we are ready to start the inference. In the Analysis Tab, we can see the overview of the sketch and run the consistency check. This check reports on potential syntactic issues (such as inconsistent variable names between the network and datasets). Once we have confirmed the consistency, we can start the inference session. 22 After starting the inference, a new window opens, taking the current state of the sketch from the editor as input. Once we start the inference, Sketchbook computes all admissible Boolean networks consistent with the specification. The tool then displays the following summary of the computation and the resulting set of candidate BNs. In this case, there is a single candidate consistent with the whole specification. In the extended summary, we see how the number of solutions evolved at various stages of the computation. Sketchbook starts the computation by symbolically encoding all interpretations of the input PSBN (before considering any static or dynamic properties). With two function symbols of arity two, we have 16 ×16 = 256 possible BNs. The tool then refines the set, filtering interpretations consistent with static properties (monotonicities and essentialities of the regulations). 23 After this, there are 4 BNs remaining (as expected, looking at the simple network). Finally, the set is further refined to only the subset of interpretations that are also consistent with all dynamic properties, leaving us with a single candidate model. We can also see the summary of admissible update functions across all the candidates. Since we only have a single candidate, only one version of each update function is possible. We can either export the symbolic representation of the resulting set of all admissible models or sample the BNs. Since there is only one candidate, let’s use the BN sampling. After downloading and opening the model file, we get the following BN in AEON format: The first part summarises the regulations (same as in the specification) and the second part the update functions. We see that the inferred update function for FRS2 is a conjunction ¬ERK∨FGFR3, and for ERK it is a disjunction RAS∨FRS2. The functions respect the selected regulation properties. If you explore the model’s state space, there are two fixed-point attractors, one with active ERK and the other with inactive ERK, as we specified. Similarly, the model can also replicate the transient ERK pulse. 24 6 Sketch Format In the first part of this section, we describe our syntax for various logical expressions that users may utilize when writing update functions or properties from scratch. We then continue by describing the formats that the tool supports for the import/export of datasets and the whole sketch. Before going into details, let’s discuss some general rules regarding identifiers. Various entities (variables, functions, ...) of the sketch can have IDs, names, and annotations. An ID is a unique combination of alphanumeric characters and underscores; an ID should not start with a number. The name is an arbitrary combination of characters; we only require it not to contain newlines. An annotation is a completely arbitrary string. 6.1 Logical expressions and languages 6.1.1 Syntax of update functions Each variable has an update function that dictates its behaviour. Update functions are logical expressions in the format given by the following grammar. Note that varId is an ID of some variable and fnId is an ID of a function. function =(function )|const |varId |fnSymbol |!function |function OP function const =true |false OP =&|||=> |<=> fnSymbol =fnId(args) args =function |args, args For example, the update function C→(B∧h(A, C)) could be written as: C => (B & h(A,C)) 6.1.2 Syntax of generic dynamic properties Users can define generic dynamic properties using the logic HCTL. For user convenience, we also support certain “template meta-expressions” (or shortcuts) corresponding to various property templates. This way, users can use shortcuts for trajectory or attractor formulas. We provide details on these shortcuts at the end of this subsection. The following grammar defines our textual format for HCTL formulae: formula =(formula )|const |propName |var |unaryOp formula |formula binaryOp formula |formula binaryOp formula |%templateExpression% const =true |false var ={varName} unaryOp =∼ | AX |EX |AF |EF |AG |EG binaryOp =&|||=> |<=> |^|AU |EU hybridOp =!|3|V|@|\bind |\exists |\forall |\jump Note that varName stands for an HCTL variable, while propName stands for an atomic proposition. Each propName must correspond to a valid BN variable ID (this is checked). Only alphanumeric 25