[{"_1":2,"_181":-5,"_182":-5},"loaderData",{"_3":4,"_17":18,"_25":26,"_160":161},"root",{"_5":-5,"_6":-7,"_7":8,"_9":-7,"_10":11,"_12":-7,"_13":14,"_15":16},"currentUser","primaryEmail","siteVerification","6LeIxAcTAAAAAJcZVRqyHh71UMIEGNQ_MXjiZKhI","toast","enableDev",false,"incidentStatus","theme","system","contrast","normal","routes/_layout",{"_19":-5,"_20":21,"_22":21,"_23":11,"_24":21},"username","isAskGordonEnabled",true,"isUsingNewTemplate","showMinimalLanding","showHoneypotTrap","routes/_layout.r.$namespace.$reponame",{"_27":28,"_29":-5,"_30":11,"_31":11,"_32":33,"_34":35,"_36":-5,"_37":11,"_38":39,"_88":89,"_111":112,"_149":-5,"_150":11,"_151":21,"_152":11,"_153":-5,"_154":11,"_155":-5,"_156":157,"_158":113,"_159":-7},"canonicalUrl","https://hub.docker.com/r/mclab/linearizer-benchmark/tags","mcpServer","canSeeDockerfile","canSeeAutobuilds","namespace","mclab","reponame","linearizer-benchmark","cloudBuildSource","isAutobuildsAvailable","repo",{"_40":41,"_42":43,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":55,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":62,"_64":65,"_66":-5,"_67":68,"_69":70,"_71":11,"_72":33,"_73":74,"_79":21,"_80":81,"_85":33,"_86":87},"categories",[],"content_types",[44],"image","date_registered","2016-11-01T23:36:16.067874Z","description","Benchmark reproducing experiments from our paper \"Linearising Discrete Time Hybrid Systems\".","is_private","last_updated","2018-09-21T12:00:56.852193Z","last_modified","2024-10-16T13:48:34.145251Z","media_types",[56],"application/vnd.docker.container.image.v1+json","name","pull_count",3399,"repository_type","star_count",1,"status","status_description","active","source","collaborator_count",0,"full_description","====================\nLinearizer Benchmark\n====================\n\n.. contents::\n\nThis repository contains benchmark reproducing experiments from our paper\n\"Linearising Discrete Time Hybrid Systems\"\nsubmitted to IEEE Transactions on Automatic Control.\n\nTo provide faithful reproduction of our experiments and easy execution on any platform we packaged benchmark as a software container.\nThe only needed prerequisite for its execution is `Docker `_,\nthat can be installed using instructions from\n`the official website `_.\n\nAfter Docker installation you need to perform following steps to execute the benchmark:\n\n1. Build the image:\n::\n\n docker build -t mclab/linearizer-benchmark .\n\nAs an alternative you can download a prebuilt image from official docker hub:\n::\n\n docker pull mclab/linearizer-benchmark\n\n2. Run the container:\n::\n\n docker run --rm -it mclab/linearizer-benchmark\n\nNow you are inside the shell of the benchmark container.\nFrom here you can execute different parts of the benchmark described below.\n\nEvaluation of linearisation algorithm\n=====================================\n\nThis part of the benchmark evaluates performance of our linearisation algorithm implemented in `linearizer `_ library.\n\nLinearisation of :math:`y \\cos{x}`\n----------------------------------\n\nTool ``lin_benchmark_1`` computes linearisation of the function :math:`y \\cos(x)`\non the interval :math:`[0,2\\pi]\\times[-\\alpha,\\alpha]`.\n::\n\n Usage:\n lin_benchmark_1: --alpha= --eps= -m -o \n lin_benchmark_1: -h|--help\n\n --alpha= y ranges in [-alpha,alpha]\n --eps= error threshold\n -m number of sampling points\n -o output file\n -h, --help print help message\n\nExample invocation that computes linearisation of :math:`y \\cos(x)`\non the interval :math:`[0,2\\pi]\\times[-2,2]`\nusing :math:`\\varepsilon=0.1` as upper bound for linearisation error\nand :math:`m=80` number of sampling points:\n::\n\n lin_benchmark_1 --alpha=2 --eps=0.1 -m 80 -o lin.txt\n\nDuring the execution tool reports the current progress, number of intervals in the cover, CPU time and peak RAM usage.\n::\n\n Progress n CPU (sec) RAM (KB)\n 0.10% 5 0.0511 36648\n 0.15% 7 0.0632 36648\n ...\n\n\nThe output is a text file with very simple format.\nFirst line contains two numbers: the number of intervals in the computer cover and the arity of the input function.\nThe rest of the file tool fills line by line with the elements of the following matrices:\n\n1. matrix representing lower bounds of the cover intervals\\(element :math:`(i,j)` is the lower bound of :math:`i`-th interval for :math:`j`-th dimension)\n2. matrix representing upper bounds of the cover intervals (element :math:`(i,j)` is the upper bound of :math:`i`-th interval for :math:`j`-th dimension)\n3. matrix representing under-approximation\n4. matrix representing over-approximation\n\nSource code of the tool is available in the directory ``linearisation/src``.\n\nTerm-wise approach\n------------------\n\nTool ``lin_benchmark_2`` computes linearisation of the function\n:math:`\\sum_{i=1}^{t} x_{i} x_{i+1}`.\n\nThis can be done\n\n* giving this function as it is to the linearisation algorithm (*monolithic* approach)\n* treating each element of the sum separately (*term-wise* approach)\n\n::\n\n Usage:\n lin_benchmark_2: -t -w --eps= -m -o [--term-wise]\n lin_benchmark_2: -h|--help\n\n -t number of terms (1..4)\n -w x_{i} ranges in [-w,w]\n --eps= error threshold\n -m number of sampling points\n -o output file\n --term-wise use term-wise approach\n -h, --help print help message\n\n\nExample invocation that computes linearisation of\n:math:`x_1x_2+x_2x_3+x_3x_4`\non the interval :math:`[-2,2]^{4}`\nusing term-wise approach and\n:math:`\\varepsilon=1.0` as upper bound for linearisation error\nand :math:`m=10` number of sampling points:\n\n::\n\n lin_benchmark_2 -t 3 -w 2 --eps=0.1 -m 10 -o lin.txt --term-wise\n\nThe execution log format and output format are the same as of ``lin_benchmark_1``.\nThe only difference is that when term-wise approach is used, :math:`t` output files are produced, one for each term.\n\nSource code of the tool is available in the directory ``linearisation/src``.\n\n\nControl software synthesis\n==========================\n\nThis part of the benchmark demonstrates how our linearisation approach combined with\n`QKS `_\ntool can be used to automatically generate control software\nfor a non-linear Discrete Time Hybrid System.\n\nOur workflow consists of following steps:\n\n1. Linearisation\n2. Replication of transition relation\n3. Controller synthesis\n4. Simulation of closed loop system\n\nWe apply this workflow to the model of inverted pendulum with different frictions.\n\nIn the paper we presented 3 experiments with following configurations\n(:math:`\\varepsilon` is the upper bound for linearisation error,\n:math:`b` is the number of quantization bits):\n\n1. :math:`\\varepsilon=0.5` and :math:`b=8`\n2. :math:`\\varepsilon=0.5` and :math:`b=9`\n3. :math:`\\varepsilon=1.1` and :math:`b=9`\n\nOther parameters in all experiments were chosen as follows:\n\n* simulation step :math:`\\tau=0.01`\n* controller sampling time :math:`T=0.1`\n* friction coefficient above pivot point :math:`\\mu_1=0.01`\n* friction coefficient below pivot point :math:`\\mu_2=0`\n* torquing force intensity :math:`F=0.5`\n\nFor each experiment there is a directory inside\n``control_software_synthesis/hybrid`` that contains input and output for each workflow step.\n\nBelow you can find detailed description of each step.\n\nLinearisation\n-------------\n\nWe use our tool ``lin4qks`` to computer DTLHS overapproxmating initial DTHS model.\nMore information about it can be found\n`here `_.\n\nExample invocation:\n::\n\n lin4qks -i input/model.m -f input/functions.c -o output/model.m\n\nHere lin4qks takes as input file ``input/model.m``, reads definitions of the functions from ``input/functions.c``\nand writes the output DTLHS to ``output/model.m``.\n\nReplication of transition relation\n----------------------------------\n\nAfter obtaining DTLHS model at the previous step we continue replicating its transition relation :math:`k` times in such way that\n:math:`T=k\\tau` where :math:`T` is desired controller sampling time and :math:`\\tau` is simulation step.\n\nTool ``replicate4qks`` takes as input the file with the model and how many times to replicate its transition relation.\nIt outputs model with replicated transition relation together with file containing computed bounds for new variables introduced.\n\nExample invocation:\n\n::\n\n replicate4qks -i input/model.m -o output/model.m -b output/computed_bounds.txt -n 10\n\n\nController synthesis\n--------------------\n\nFinally ``QKS`` is used to automatically synthesize control software.\n\nExample invocation:\n::\n\n qks -d input -dk output -no_compute_bounds -on_the_fly\n\n``QKS`` will generate control software (files ``ctrl.h`` and ``ctrl.c``) in the ``output`` directory.\n\nSimulation of closed loop system\n--------------------------------\n\nFor the experiment #2 (:math:`\\varepsilon=0.5` and :math:`b=9`) in which ``QKS`` succeeded to find controller we performed also simulation of plugging generated control software into `OpenModelica `_-based simulator.\n\nSimulator can be found in directory ``control_software_synthesis/hybrid/simulator``:\n\n* ``plant.mo`` is the model of the inverted pendulum.\n* ``controller.mo`` is modelica wrapper for our C control software.\n* ``closed_loop.mo`` is the model that couples together plant and controller.\n\nFiles ``ctrl.h`` and ``ctrl.c`` generated by ``QKS`` must be put into ``Resources/Include``.\n\nSimulation can be started by running ``omc run.mos``\n\nControl software synthesis for switched systems\n===============================================\n\nThis part of the benchmarks is aimed at comparison of our approach with the state-of-the-art tool `PESSOA `_.\n\nBy setting :math:`\\mu_1=\\mu_2=0.01` in our model of the inverted pendulum we get a switched system without mode jumps.\n\nWe run 1 experiment with ``PESSOA`` and 2 experiments with ``QKS``. In all expeirments we used the same sampling time :math:`T=0.1`.\n\nPESSOA\n------\n\nExperiment configuration:\n\n* state quantization :math:`0.0138` (that corresponds to 9 bits for the angle and 10 bits for the velocity)\n* input range :math:`[-0.5,0.5]` and input quantization :math:`0.5`\n\nNote that this experiment cannot be reproduced inside Docker container, since we cannot redistribute MATLAB environment. To run this experiment navigate inside MATLAB to the directory with the input files and execute ``InvPend`` command.\n\nInput and output files can be found in ``control_software_synthesis/switched/pessoa``.\n\nList of the input files:\n\n* ``InvPend.m``\n* ``pss_dynamics.m``\n* ``dynamic.m``\n\nList of the output files:\n\n* ``InvPend.bdd`` is the OBDD for the abstraction\n* ``InvPendTargetSet.bdd`` is the OBDD for the target set\n* ``InvPendController.bdd`` is the OBDD for the controller\n\nAlso in the same directory you can find Simulink model ``closed_loop.mdl`` that allows simulation of the closed loop system obtained with the generated controller, using S-Function block provided together with PESSOA.\n\n\nQKS\n---\n\nWe run 2 experiments with ``QKS`` with :math:`\\tau=0.01` and with :math:`\\tau=0.1`. In both experiments we used linerisation computed with :math:`\\varepsilon=0.1` as error threshold resulting in 8 intervals. We used 9 bits for state quantization and torquing force intensity :math:`F=0.5`.\n\nInput and output files for the each step of the control software synthesis flow can be found in ``control_software_synthesis/switched/qks``.\n\nFor these experiments we also provide Simulink model for simulation: ``closed_loop.mdl``. Before using it, first copy the needed ``ctrl.c`` and ``ctrl.h`` files (``QKS`` controller) in the same folder as ``closed_loop.mdl`` and then compile ``QKS`` controller and S-Function into MATLAB MEX executable file:\n::\n\n mex ctrl_sfunction.c ctrl.c","has_starred","hub_user","immutable_tags_settings",{"_75":11,"_76":77},"enabled","rules",[78],".*","is_automated","permissions",{"_82":21,"_83":11,"_84":11},"read","write","admin","user","storage_size",1811999666,"orgData",{"_90":91,"_92":93,"_94":95,"_96":33,"_97":98,"_99":100,"_101":102,"_103":104,"_105":106,"_107":98,"_108":98,"_109":98,"_110":21},"id","5af353fe65274554bc6072948ccf5a38","uuid","5af353fe-6527-4554-bc60-72948ccf5a38","type","organization","orgname","full_name","","location","Computer Science Department, Sapienza University of Rome","company","Model Checking Laboratory","profile_url","http://mclab.di.uniroma1.it/","date_joined","2015-05-05T11:30:21.809769Z","gravatar_url","gravatar_email","badge","is_active","recentTags",[113],{"_114":44,"_115":116,"_117":118,"_90":119,"_120":121,"_50":138,"_139":116,"_140":33,"_141":56,"_57":142,"_143":144,"_145":129,"_146":138,"_147":65,"_148":21},"content_type","creator",294977,"full_size",445313668,5835653,"images",[122],{"_123":124,"_125":126,"_127":98,"_128":129,"_130":131,"_132":133,"_134":98,"_135":-5,"_136":118,"_63":65,"_137":-5},"architecture","amd64","digest","sha256:4a452abaf489cc40fdd2d91820b0120699a7e0696356ca3b18d369a7c37cfbbc","features","last_pulled","2026-10-07T11:14:02.792344869Z","last_pushed","2018-09-21T12:00:36Z","os","linux","os_features","os_version","size","variant","2018-09-21T12:00:35.181008Z","last_updater","last_updater_username","media_type","latest","repository",1018999,"tag_last_pulled","tag_last_pushed","tag_status","v2","sbxKitMetadata","isPotentialSpam","isHubSbxKitsEnabled","showSbxLogoOverride","sbxTrademarkText","displaySecurityMetadata","tagAttestations","tagsHaveAttestations",[],"selectedTag","attestationsUrl","routes/_layout.r.$namespace.$reponame.tags",{"_38":162,"_169":170,"_156":179,"_180":11},{"_40":163,"_42":164,"_45":46,"_47":48,"_49":11,"_50":51,"_52":53,"_54":165,"_57":35,"_32":33,"_58":59,"_60":44,"_61":62,"_63":62,"_64":65,"_66":-5,"_67":68,"_69":70,"_71":11,"_72":33,"_73":166,"_79":21,"_80":168,"_85":33,"_86":87},[],[44],[56],{"_75":11,"_76":167},[78],{"_82":21,"_83":11,"_84":11},"tags",{"_171":62,"_172":-5,"_173":-5,"_174":175},"count","next","previous","results",[176],{"_114":44,"_115":116,"_117":118,"_90":119,"_120":177,"_50":138,"_139":116,"_140":33,"_141":56,"_57":142,"_143":144,"_145":129,"_146":138,"_147":65,"_148":21},[178],{"_123":124,"_125":126,"_127":98,"_128":129,"_130":131,"_132":133,"_134":98,"_135":-5,"_136":118,"_63":65,"_137":-5},[],"canDeleteTags","actionData","errors"]

mclab/linearizer-benchmark

Tags for mclab/linearizer-benchmark