The capture and prediction of rainfall-induced landslide warning signals is the premise for the implementation of landslide warning measures. An attention-fusion entropy weight method (En-Attn) for ...capturing warning features is proposed. An attention-based temporal convolutional neural network (ATCN) is used to predict the warning signals. Specifically, the sensor data are analyzed using Pearson correlation analysis after obtaining data from the sensors on rainfall, moisture content, displacement, and soil stress. The comprehensive evaluation score is obtained offline using multiple entropy weight methods. Then, the attention mechanism is used to weight and sum different entropy values to obtain the final landslide hazard degree (LHD). The LHD realizes the warning signal capture of the sensor data. The prediction process adopts a model built by ATCN and uses a sliding window for online dynamic prediction. The input is the landslide sensor data at the last moment, and the output is the LHD at the future moment. The effectiveness of the method is verified by two datasets obtained from the rainfall-induced landslide simulation experiment.
The Bainiuchang Ag polymetallic deposit is located at the junction between the Cathaysia, Yangtze, China and Indosinian blocks. It has experienced many geological events, and records excellent ...conditions for multiple mineralization. In this paper, elemental correlation analysis, cluster analysis, factor analysis, a semivariogram of Zn/Pb values, mineralization distribution and trend surface analysis have been carried out based on the prospecting database and ore body model. Our results show that Ag–Pb–Zn were mineralized at moderate temperatures. Tin was mineralized at high temperatures, and Sn and Zn/Pb values are well correlated. The Zn/Pb values can be used for tracing the ore-forming fluid. The semivariogram revealed that the Zn/Pb values are moderately spatially dependent, with good mineralization continuity in the 100° and 10° directions. The spatial pattern of the elemental grade correlates with mineralization enrichment. The trend surface analysis shows that the Ag, Pb, Zn, and Cu mineralization is weak in the south and strong in the north of the deposit, and the Sn grades and Zn/Pb values are high in the south and low in the north. High-temperature Sn, medium-temperature Cu, and medium-temperature Ag–Pb–Zn mineralization have occurred in a south-to-north trend. Therefore, the source of the ore-forming fluid was in the southern part of the mining area. During the migration of the ore-forming fluid from south to north, different minerals were precipitated due to changes in the physicochemical environment. The spatial patterns of mineralization may provide a basis for studying the formation of the ore deposit, and can guide ore exploration and mining in the mine area and similar ore deposits elsewhere.
In the domain of reinforcement learning (RL), deriving efficacious state representations and maintaining algorithmic stability are crucial for optimal agent performance. However, the inherent ...dynamism of state representations often complicates the normalization procedure. To overcome these challenges, we present an innovative RL framework that integrates state normalization techniques with residual connections and incorporates attention mechanisms into generative adversarial imitation learning (GAIL). This combination not only enhances the expressive capability of state representations, thereby improving the agent’s accuracy in state recognition, but also significantly mitigates the common issues of gradient dissipation and explosion. Compared to traditional RL algorithms, GAIL combined with the residual connection-based state normalization method empowers the agent to markedly reduce the exploration duration such that feedback concerning rewards in the current state can be provided in real time. Empirical evaluations demonstrate the superior efficacy of this methodology across various RL environments.
Functional movement screening (FMS) is a crucial testing method that evaluates fundamental movement patterns in the human body and identifies functional limitations. However, due to the inherent ...complexity of human movements, the automated assessment of FMS poses significant challenges. Prior methodologies have struggled to effectively capture and model critical human features in video data. To address this challenge, this paper introduces an automatic assessment approach for FMS by leveraging deep learning techniques. The proposed method harnesses an I3D network to extract spatiotemporal video features across various scales and levels. Additionally, an attention mechanism (AM) module is incorporated to enable the network to focus more on human movement characteristics, enhancing its sensitivity to diverse location features. Furthermore, the multilayer perceptron (MLP) module is employed to effectively discern intricate patterns and features within the input data, facilitating its classification into multiple categories. Experimental evaluations conducted on publicly available datasets demonstrate that the proposed approach achieves state-of-the-art performance levels. Notably, in comparison to existing state-of-the-art (SOTA) methods, this approach exhibits a marked improvement in accuracy. These results corroborate the efficacy of the I3D-AM-MLP framework, indicating its significance in extracting advanced human movement feature expressions and automating the assessment of functional movement screening.
There are two different types of programs: imperative programs that describe how to solve a problem, like C or Java, and declarative programs that describe how to recognize that the problem is ...solved, like SQL or Alloy. The inherent difference between them leads to different analysis techniques. Despite the large number of debugging techniques and tools developed for imperative programs, there is a dearth of tools for declarative programs. In this dissertation, we develop tools to ensure correctness and improve reliability for both imperative and declarative programs. For imperative programs, we focus on automatically inferring program invariant. Program invariant, which describes program states or behaviors as mathematical formulas, is one main approach to verifying and debugging imperative programs. However, the current invariant generation techniques focus on numerical invariants described by Hoare Logic, lacking support for memory-related properties. We present SLING, a dynamic analysis tool to automatically infer program invariant described by Separation Logic, an extension of Hoare logic with a compact description for memory properties. The empirical results show that SLING can efficiently discover invariants for pointers and data structures and the generated invariant can be used automatically to repair corrupted data structures. For declarative programs, we focus on automatically debugging Alloy specifications. Alloy is a declarative specification language widely used in various software problems. However, unlike imperative programs, there is a dearth of techniques to help to debug Alloy specifications. We present FLACK to automatically locate Alloy bugs and ATR to repair them. Experimental results show that FLACK can accurately locate buggy expressions and ATR can effectively repair different types of bugs.
The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite ...significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, exploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state-of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of real-world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.
Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for ...imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not "executed," but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real-world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions).
BeAFix Brida, Simon Gutierrez; Regis, German; Zheng, Guolong ...
2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE),
11/2021
Conference Proceeding
This paper describes BeAFix, a tool for automated repair of faulty Alloy models. The tool builds upon the Alloy Analyzer, the analysis tool for Alloy. It generates repair candidates by mutating a ...faulty Alloy model, and employs a bounded-exhaustive approach to traverse the space of repair candidates. Since BeAFix's mutation operators make the space of repair candidates to quickly grow, the tool supports some sound pruning techniques, that allow it to fix Alloy models with more than one faulty line or expression. Additionally, BeAFix does not require tests as a patch acceptance criterion. Although BeAFix supports tests as oracles, our tool is also able to leverage property-based oracles, which are more commonly found in Alloy models in the form of predicate satisfiability and assertion validity checks.
A video demonstration of BeAFix can be found at https://youtu.be/5RG40SmlFXQ. The tool's binaries and further details about its usage, can all be found at https://sites.google.com/view/beafixevaluation/beafix. The tool is also available in a public archive at https://doi.org/10.5281/zenodo.5296466.
PDF
