dataesr/scientific-paragraphs-categorization huggingface dataset:
The module also recovers the protein sequence of each input ID. Each protein and gene ID listed on this web page are linked to corresponding UniProt and NCBI web pages. FASTA amino acid sequences of each input are also downloadable. The module dedicated to the functional annotation according to the GO consortium, produces results that are viewed on the "GO" web page of ProteINSIDE. ProteINSIDE imports GO terms by querying the QuickGO database  [38]. QuickGO was chosen because of its daily update, accessibility, and performances. ProteINSIDE only imports GO terms that have been selected by evidence codes (GO Inferred from Electronic Annotation codes (IEA) are excluded by the basic analysis) and confirmed by curators. The GO script of ProteINSIDE analyses over-and under-represented terms to identify the most relevant and the most specific terms associated with the uploaded list.
Within a GO, ProteINSIDE compares the number of genes or proteins from the dataset to the total number of gene products (for a species) declared in the AmiGO database  [29]  to provide a coverage frequency, and thus, to identify the most representative pathways associated to a dataset. The result is viewed on the "GO" web page of ProteINSIDE as tables and diagrams. Three tables (Figure  5 ) report the GO terms that annotated two or more proteins (Figure  5-B ), the GO terms that annotate one protein (Figure  6-C ), as well as all GO terms for a protein (Figure  5-D ). Each annotation is informed with an evidence code (that reflects the type of experimental evidence or analysis to describe an annotation between a GO term and a gene product) and the database source. Tables are automatically sorted by the best enrichment p-value to help the user to view the most significant GO terms related to a dataset.
Tables can also be sorted by ontology group, p-value range for enrichment, GO term description, gene name or any input IDs (Figure  5B ). From the sample dataset of 132 proteins, ProteINSIDE annotated 128 proteins with 624 GO terms. The most significant enriched GO terms is "hormone activity" (that annotated 31 proteins over the 79 expected; not shown) and "glycolytic process" (that annotated 27 proteins over the 33 expected; Table  1 ). The low number of annotated proteins may be related to our choice to use only GO terms that have been confirmed by curator in the basic analysis. This means that the basic analysis doesn't use the annotation with IEA (Inferred by Electronic Annotation) evidence code. However, the option to use IEA is provided in the custom analysis to extend the annotations.
For this purpose, we have selected about 1,000 GO terms related to secretion (monthly updated) as for example: secretion, vesicle, or extracellular region. This four-step analysis improves the reliability of proteins proposed to be secreted thanks to a signal peptide and to our knowledge is unique to ProteINSIDE  [40]. However, proteins are also secreted by pathways that do not involve signal peptide such as: endosomal recycling, plasma membrane transporter, membrane flip-flop, and membrane blebbing including the formation of vesicles or exosomes  [41]. Thus, ProteINSIDE was designed to predict the proteins secreted by other pathways, by gathering the data of subcellular location provided by UniProt, GO terms, and TargetP results (Figure  6-B ). From our sample dataset of 132 proteins, ProteINSIDE has predicted 85 proteins as potentially secreted outside the cell by a signal peptide, among them 78 over the 79 proteins that were expected (Table  1 ).
The basic analysis identifies PPi within the uploaded dataset (core network) using the preselected databases IntAct, UniProt, and BioGrid. These PPi databases were chosen as a default option because there are daily updated and reviewed by curators as well as by the curation processes of the IMEx project (that ensures reliable interactions data using experts and curation rules shared between many interaction databases  [26] ) or MIMIx (a guideline of the minimum information required for reporting a molecular interaction experiment, thus advising the user on how to use the interaction data  [27] ). Moreover, BioGrid is the biggest PPi database that has its own curation workflow (more than 740000 curated PPi) and is not a partner of IMex curation program. IntAct is another big PPi database with more than 380000 PPi currated according to IMex and MIMIx curation rules and that are often listed in several databases.
UniProt is a major database dedicated to the study of proteins. Thus, it possesses its own curated PPi but in lesser amounts compared to the two other specialized databases (less than 13 000 PPI; UniProt is a partner of IMEx project). By using 3 databases as a default option, the aim of ProteINSIDE is to favour the use of multiple PPi databases in order to improve the PPi data gathering  [42]. These 3 PPi databases ensure the good recovery of known interactions for an overview of interactions within or/and outside of a new dataset. Then, ProteINSIDE lists pairs of proteins known to interact between each other in a downloadable table (Figure  7 ) and constructs a network (Figure  8 ) using the PPi identified within the uploaded list. The dynamic network is available by using the "Cytoscape" button on the "Protein Interaction" web page ("Dynamic Cytoscape view of PPi", Figure  7-A ).
Within the network, edges are experimental detection methods used to identify the PPi. Consequently, several edges may link two proteins. Network can be sorted by the number of interactions by node, the proximity of a node to other nodes (closeness centrality; CC) and the shortest paths between nodes (betweenness centrality; BC) (Figure  8-A ). These centralities criteria were already proven to be efficient to select key nodes/proteins within a pathway  [43]. From our sample dataset of 132 proteins, ProteINSIDE has identified 29 PPi that involved 28 different proteins (Figure  7-B ). As expected from our small dataset, ProteINSIDE linked, within sub networks, proteins involved in glycolysis, TCA or respiratory chain as protein complexes (partially on Figure  8-B ).
Setting up a Custom Analysis: an addedvalue provided by the extension of the analysis We made a custom analysis using the same major settings as for the basic analysis with additional options (GO network, GO electronic annotations, and extension of PPi to proteins outside of the dataset in the same species, extended network). To set up the custom analysis, user has to follow these steps (also explained by Figure  2 ):  Click on the "Custom Analysis" menu on the homepage of ProteINSIDE  Fill in "the job name" box  Select the species of study (the same species as the uploaded IDs)  Upload an input file or directly paste IDs Then, user has to select the settings of either all or only one module of analysis on the section "4" of the page, by following these steps (Figure  9 ):   B  and C ) GO terms are also sorted as two dynamic tables (a table for GO terms that annotate more than one protein on the dataset -B, and a second table for the GO terms with a single protein annotated -C).
 Select Gene Ontology module o Select "GO electronic annotation (IEA)" if you aim to use GO annotation inferred from electronic annotation. o Select "Gene Ontology Tree network" to view linked GO terms  Select Signal peptide module to use the basic cutoff value of prediction  Select Protein -protein interaction module o Select "Protein -protein interaction custom analysis" o Select "Extend PPi research using protein outside of the dataset", if wanted o Select "Human species" to analyse PPi using data available in Human, for example o Select either the 3 most used databases (IntAct, UniProt, and BioGrid as used in the basic analysis) or from 1 to 31 databases (PPi are daily updated in each database) Alternatively, user can load automatically the same settings as those already used in a previous custom analysis, by clicking on the "pre-set" button.
The network can be sorted by ontology group, by p-value range (to select and to link only the most enriched GO terms), by the number of directly linked terms or also by the number of GO terms linked together (to select group of GO terms involved in the same biological function). From our sample dataset, we have chosen to illustrate the GO tree of the "Molecular Function" group (Figure  10 ). In this visualisation, squares with dark red colour were GO terms which have annotated the highest number of proteins. Among them and as expected the GO:0005179 with the best p-value and the darkest red colour was "Hormone activity", in agreement with the over representation of hormones in our sample dataset. The "Secreted Proteins" module has predicted the same 85 proteins as the basic analysis as being secreted.
By comparison with the basic analysis, the use of IEA option has allowed to confirm this prediction for 82 proteins that were also annotated with GO terms related to a "secretion" function. By comparison with the basic analysis, the settings selected within the "Protein Interaction" module provided PPi within the dataset (between proteins of the dataset, as the basic analysis) and PPi between proteins from the dataset and outside of the dataset. For the extended network, ProteINSIDE retrieved 688 PPi made by 500 proteins. Among them, 61 proteins were from our uploaded sample dataset. By using PPi outside of the dataset in Human species, we got 95% more PPi that involved 60% more proteins from the sample dataset than the PPi recovered with the basic analysis. The extended network (Figure  11 ) highlighted major subnetworks related to the respiratory chain (Figure  11-A ), hormone activity such as signalization pathways of adipokines (Figure  11-B ), growth hormone (Figure  11-C ), thyroid hormones (Figure  11-D ), glycolysis (not highlighted), and carbohydrate metabolism (not highlighted).
The DAVID  [59] , ToppGene  [12]  or Babelomics  [60]  software resources are often mentioned for the biological knowledge gathering, functional annotation using GO terms or searches for proteins interactions. By comparison to these tools, added-values of ProteINSIDE have to be highlighted. ProteINSIDE provides a functional annotation using a monthly updated GO terms database and enrichment calculation. Indeed, the list of GO terms is in constant evolution and GO terms could become redundant or obsolete the next month  [15]. This could induce bad information in the results of an analysis if the database is not often updated. Each result of the annotation is easily readable thanks to dynamic tables and diagrams which can be sorted with many options and can be downloaded to work offline. The GO tree visualization of the most often associated GO terms with a list of IDs, is another added-value of ProteINSIDE.
Tree networks of GO terms are also done by AmiGO or QuickGO to get an ancestor chart of a single term. However, ProteINSIDE is the only tool which highlights biological pathways of a dataset using linked GO terms and their representativeness rate (using p-values and number of annotations). This network visualization is also easy to use thanks to the friendly user interface that gives access to the sort options. For the PPi research and visualization, ProteINSIDE uses only interactions that are based on experimental observations. The drawback is that the number of PPi identified by ProteINSIDE could be lower than those proposed by other resources that also list predicted interactions inferred from literature mining. Furthermore, ProteINSIDE is also capable to draw large interaction networks thanks to the use of the powerful graphical Cytoscape application.
For this, ProteINSIDE automatically selects homologous IDs from its database for the wanted species. Nevertheless, user can choose to run a local Blastp to select the species with the highest sequence homology with the proteins of the input dataset, and then ProteINSIDE proceed to the selection of orthologous IDs for this species. A functional annotation of all proteins from an extended network (PPi between proteins within and outside of the dataset) is done by clicking a button on the network visualisation. Results of this annotation are available as a new analysis. In addition to biological knowledge gathering, GO annotation, and analysis of PPi, ProteINSIDE also proceeds to an in silico secretome analysis  [40]. For this purpose, ProteINSIDE merges four strategies of analysis: signal peptide  [16]  and cellular location  [22]  predictions, as well as a review of GO term annotation and cellular location recorded in UniProt.
Thus, IDs from these species are perfectly recognized and analysed by ProteINSIDE. To our knowledge, ProteINSIDE is the only resource that allows the user to recover biological knowledge from well-known species (human, rat or mouse) using IDs from ruminant species. This avoids losing information since many sequences or annotations remain to be stored in public databases for ruminant species and especially for goat. To our knowledge, only AgBase  [61] , a manually curated gene annotation database for farm species, including cattle and sheep, is available for functional annotation. However, AgBase does not perform analysis of PPi or prediction of secreted proteins. In this article we have presented the performances of ProteINSIDE, a new powerful workflow which gathers tools and public databases to retrieve biological information of genes or proteins lists from 6 species (Bovine, Ovine, Caprine, Human, Rat, and Murine).
Identified peptides can be "noTM" (not transmembrane) or "TM" (transmembrane), only "noTM" are listed in the first table. The column "Subcellular location" provides the location of the protein declared in the UniProt database. The column "TargetP" provides the prediction of the subcellular location of the protein by TargetP software, and GO related to secretion are also listed to improve the prediction. A second table lists proteins with the "TM" prediction of SignalP, not shown in the figure since there was no result with the sample dataset. (B) A third table lists proteins potentially secreted by secretory pathways that do not involve signal peptide. In this table, GO terms, TargetP prediction, and subcellular location are also selected to improve the prediction. Firstly, user has to enter a name for the analysis, select the species of study, and directly paste the input IDs (Figure  2 ).
Figure10. GOTree network visualization. Linked GO terms which annotate the dataset are linked using ancestor chart method. Each edge means that a term A is a subtype of a term B (is_a). Information about a GO is obtained by clicking on the GO or the node. Red colour is only for the GO terms relative to the Molecular Function. The degree of colour saturation is related to the number of proteins annotated by a GO (dark and clear for high and low numbers, respectively).
Formal process languages inheriting the concurrency and communication features of process algebras are convenient formalisms to model distributed applications, especially when they are equipped with formal verification tools (e. g. , modelcheckers) to help hunting for bugs early in the development process. However, even starting from a fully verified formal model, bugs are likely to be introduced while translating (generally by hand) the concurrent model -which relies on high-level and expressive communication primitives-into the distributed implementation -which often relies on low-level communication primitives. In this paper, we present DLC, a compiler that enables distributed code to be generated from models written in a formal process language called LNT, which is equipped with a rich verification toolbox named CADP.
Such interactions are often abstracted away in the formal models, while a real interaction is required in the final implementation. For instance, consider a distributed system where some process deals with a database. In the formal model, the database may be abstracted away by read and write operations. However, we want the implementation of these processes to actually connect to an external database which is independently developed from the distributed system under study. The compiler should provide a mechanism to define interactions with the external environment and embed them in the final implementation. Third, the generated implementation must achieve reasonable performances for rapid prototyping. Even though the aim is not to compete with hand-crafted optimized implementations, a too important performance penalty would make the rapid prototyping approach irrelevant.
LNT models can be formally verified using software tools available in the CADP  1  (Construction and Analysis of Distributed Processes)  [4]  tool box, which provides simulation, model-checking, and test generation tools, among others. LNT enables a high-level description of nondeterministic concurrent processes that run asynchronously (i. e. , at independent speeds, as opposed to synchronous processes cadenced by a global clock), and that interact by rendezvous (also called synchronization) on actions. The rendezvous mechanism of LNT is expressive and general: • A rendezvous may involve any number of processes (multiway rendezvous), i. e. , it is not restricted to binary synchronizations. LNT even features n-amongm synchronization  [5] , in which a rendezvous may involve any subset of n processes out of a larger set of m.
We introduce DLC (Distributed LNT Compiler), a new tool that achieves automatic generation of a distributed implementation in C from an LNT model. We focus on LNT since we think its roots in process algebra offer a well-grounded basis for formal study of concurrent systems  [6] , and because it is already equipped with the numerous verification features of our team's toolbox CADP, which however still lacks distributed rapid prototyping. Nonetheless, our approach should be relevant to any language whose inter-process communication and synchronization primitive is multiway value-passing rendezvous. DLC meets the three challenges stated earlier: • DLC transforms each concurrent process of the distributed system model into a sequential program, and instantiates an elaborate protocol to handle multiway rendezvous.
The protocol we use  [7]  is not a new contribution, though it is extended to handle n-amongm rendezvous and data exchange. The generated programs can run on several distinct machines. • Interactions with the external environment are made possible through calls to user-defined external procedures. With DLC, the user can define hook functions that are integrated in the final implementation and called upon actions in the system. Hook functions are written in C, and they provide a convenient way to interact with other systems. • DLC generates programs with reasonable performances, which qualify for rapid prototyping. Although generated programs execution speed may not be on par with an implementation in a classic programming language, DLC makes it possible to easily produce a validated prototype, which can be deployed and run on a cluster, from a distributed system modeled and verified using LNT and CADP.
II. RELATED WORK Several programming languages offer useful primitives or libraries for interaction between distant processes, i. e. , processes on separate machines connected by a network. The most common mechanisms are: message passing, where processes can send messages to each other, e. g. , POSIX sockets in C, or Erlang built-in messaging; and RPC (Remote Procedure Call), where a process can invoke a procedure executed by another distant process, e. g, Java RMI (Remote Method Invocation), or the "net/rpc" package of Golang standard library. However, for popular programming languages, we are neither aware of a library that would implement LNT-like multiway rendezvous, nor of a mature verification toolbox that would enable formal verification on the source code itself. We explore modeling languages equipped with both formal verification and code generation tools.
The formal study of concurrent processes is a rich field of research, and several formalisms exist to model such systems. For synchronous models, where all processes share a unique clock, a good illustration is the Esterel language, which comes with a suite of verification tools and compilers  [9]. As regards asynchronous systems, the Topo  [10]  tool set for LOTOS features code generation in either C or Ada, and enables environment interactions via LOTOS annotations. However, the generated implementation is sequential, and Topo is not maintained anymore. LOTOS is also the historical formal language of CADP, which provides the EXEC/CAESAR  [11]  tool to generate C code with interface functions that must be user-defined. Once again, this code is sequential, and our DLC tool builds upon EXEC/CAESAR (which also accepts LNT as input) for generating the code corresponding to sequential processes.
UPPAAL  [12]  provides a framework to work on networks of timed automata, including formal verification tools. The associated Times tool  [13]  generates C code from UPPAAL models, but the final program is sequential. In the framework of SPIN  [14] , Promela is a modeling language which uses channels rather than multiway rendezvous for process interactions. A Promela to distributed C compiler has been proposed  [15] , where the user must explicitly specify by hand which process is server or client. More recently, a refinement calculus to obtain C from Promela has been presented  [16] , but again the generated code is sequential. Regarding the Reo  [17]  coordination language, the Dreams  [18]  framework provides a methodology to generate distributed applications running on Java Virtual Machines.
Moreover, servers may crash and stop. In the context of Raft, the leader election is more elaborate, e. g. , the leader prevents timeouts of other servers with a heartbeat mechanism; we do not model these features here for the sake of brevity. Figure  1  illustrates the LNT model of a server. LNT syntax is close to mainstream implementation languages, and most code should be understandable for someone with a programming background. After initialization, a server enters its main loop where the nondeterministic choice operator select, reminiscent of Dijkstra  [31] , is used to enumerate several possible behaviors, separated by "[]". The server will execute one branch of the select operator, depending on its current state and the possible actions in the system. The observable events of an LNT process are actions on gates, declared between the square brackets in the process header.
Before we dig into how we generate a distributed implementation from such a model, we briefly illustrate how formal verifications can be applied to it. LNT semantics are defined formally in terms of an LTS: to any LNT process corresponds an LTS where transitions represent actions and are labeled by the gate name, followed by the exchanged data values (if any). The LTS represents the LNT model state space; since it may be huge, models are often parametrized to control the state space explosion. For instance here, the election algorithm is approximated to a smaller state space by bounding server terms with a predefined maxTerm. 2 CADP tools can perform formal verifications, e. g. , model checking, on the LTS representation, either on-the-fly or after complete state space generation. For instance, EVALUA-TOR4  [32]  can check the safety property "there is not two leaders in the same term" expressed as the following MCL (Model Checking Language)  [32]  formula: which states that, there must not be consecutive leader announcements for the same term.